[Logiweb] Error with the new base page

Kasper H0st Frederiksen tofu at diku.dk
Wed Jun 22 12:00:58 CEST 2005


I just updated my base page reference from:
http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-03-UTC-15-49-33-495567/vector/page.lgw

to:
http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw

This is the only change. Now i get a "claim failed"
and a diagnose
"Lemma expected S1'" in one of my proofs that use S1'.


I have attached the page with the error.



-Kasper Frederiksen
-------------- next part --------------
{   Logiweb, a system for electronic distribution of mathematics
    Copyright (C) 2004 Klaus Grue

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  021111307  USA

    Contact: Klaus Grue, DIKU, Universitetsparken 1, DK2100 Copenhagen,
    Denmark, grue at diku.dk, http://yoa.dk/, http://www.diku.dk/~grue/

    Logiweb is a system for distribution of mathematical definitions,
    lemmas, and proofs. For more on Logiweb, consult http://yoa.dk/.
}

PAGE logik rapport

BIBLIOGRAPHY

base:  "http://www.diku.dk/~grue/logiweb/20050502/home/grue/base/GRD-2005-06-22-UTC-06-58-05-413682/vector/page.lgw",

peano: "http://www.diku.dk/~grue/logiweb/20050502/home/grue/peano-axioms/GRD-2005-06-03-UTC-15-58-02-061312/vector/page.lgw"

PREASSOCIATIVE  base: bracket * end bracket,
test lemma,
test lemma two,
corollary one point ten a,
corollary one point ten b,
lemma one point eight,
lemma prime l three two b tmp,
lemma prime l three two b,
lemma prime l three two c tmp,
lemma prime l three two c,
lemma prime l three two d tmp,
lemma prime l three two d,
tautology one
PREASSOCIATIVE peano: system s
PREASSOCIATIVE  base: * sub * end sub
PREASSOCIATIVE  base: unicode start of text * end unicode text
PREASSOCIATIVE  base: * bit nil
PREASSOCIATIVE  base: * apply *
PREASSOCIATIVE  base: * raw head
PREASSOCIATIVE  base: * times *
PREASSOCIATIVE  base: * plus *
PREASSOCIATIVE peano: * peano plus *
PREASSOCIATIVE  base: * term plus * end plus
POSTASSOCIATIVE base: * raw pair *
POSTASSOCIATIVE base: * comma *
PREASSOCIATIVE  base: * boolean equal *
PREASSOCIATIVE peano: * peano is *
PREASSOCIATIVE  base: not *
PREASSOCIATIVE  base: * and *
PREASSOCIATIVE  base: * or *
PREASSOCIATIVE peano: peano all * indeed *
POSTASSOCIATIVE base: * macro imply *
PREASSOCIATIVE peano: * peano imply *
POSTASSOCIATIVE base: * guard *
PREASSOCIATIVE  base: * select * else * end select
PREASSOCIATIVE  base: lambda * dot *
PREASSOCIATIVE  base: * init
PREASSOCIATIVE  base: * at *
POSTASSOCIATIVE base: * infer *
PREASSOCIATIVE  base: all * indeed *
POSTASSOCIATIVE base: * rule plus *
POSTASSOCIATIVE base: * cut *
PREASSOCIATIVE  base: * proves *
PREASSOCIATIVE  base: locally define * as * end line *
POSTASSOCIATIVE base: * then *
PREASSOCIATIVE  base: * tab *
PREASSOCIATIVE  base: * row *

BODY

"File page.tex
\documentclass [fleqn]{article}
\setlength {\overfullrule }{1mm}
\input{lgwinclude}

\usepackage{latexsym}

%\setlength{\parindent}{0em}
%\setlength{\parskip}{1ex}

% The font of each Logiweb construct is under tight control except that
% strings are typeset in whatever font is in effect at the time of
% typesetting. This is done to enhance the readability of strings in the
% TeX source generated by Logiweb. The default font for typesetting
% strings is \rm:
\everymath{\rm}

\usepackage{makeidx}
\usepackage{page}
\makeindex
\newcommand{\intro}[1]{\emph{#1}}
\newcommand{\indexintro}[1]{\index{#1}\intro{#1}}
\newlength{\bracketwidth}
\settowidth{\bracketwidth}{$[{}$}
\newcommand{\back}{\protect\makebox[-1.0\bracketwidth]{}}

\usepackage[dvipdfm=true]{hyperref}
\hypersetup{pdfpagemode=none}
\hypersetup{pdfstartpage=1}
\hypersetup{pdfstartview=FitBH}
\hypersetup{pdfpagescrop={120 130 490 730}}
\hypersetup{pdftitle=Introduction to Logiweb}
\hypersetup{colorlinks=true}
\bibliographystyle{plain}

% \tex{something} writes something to page.otx for later inclusion
\newwrite\outex
\newtoks\toktex
\immediate\openout\outex=page.otx
\newcommand{\tex}[1]{\toktex={\item #1}\immediate\write\outex{\the\toktex}}

% \test{something} writes something to page.tst for later inclusion
\newwrite\outest
\immediate\openout\outest=page.tst
\newcommand{\test}[1]{\toktex={\item #1}\immediate\write\outest{\the\toktex}}

% Concerning \catcode`\@=11 : See the TeXbook, Appendix B (page 344).
% \afterheading suppresses indentation once, c.f. latex.ltx.
% \display{something} displays something as a displayed equation except
% that linebreaking is possible and displaymath is not turned on by default.
% The first paragraph after \display{something} is unindented.
% Glue below formulas may be wrong. The definition of \display misses
% something like \addvspace{\belowdisplayskip}.
\catcode`\@=11
\def\afterheading{\@afterheading}
\catcode`\@=12
\newcommand{\display}[1]{\begin{list}{}{\setlength{\leftmargin}{\mathindent}}
\item #1\end{list}

\afterheading}
\newcommand{\statement}[1]{\begin{list}{}{\setlength{\leftmargin}{0mm}}
\item #1\end{list}

\afterheading}

\begin {document}
\title {Kasper's Title}
\author {Kasper Frederiksen}
%\maketitle
%\tableofcontents
"[ ragged right expansion ]"



\section{First Section}


\subsection{Lemma "[ math lemma one point eight end math ]"}

"[ intro lemma one point eight
   index "L1.8"
   pyk   "lemma one point eight"
   tex   "L1.8"
   end intro ]"
\display{
"[ math 
  in theory system prime s
   lemma 
       lemma one point eight 
   says 
       all meta k indeed parenthesis meta k peano imply meta k end parenthesis
   end lemma 
   end math 
]"}

"[ math
     system prime s
   proof of 
     lemma one point eight
   reads
     arbitrary meta k end line
     line ell a because axiom prime a two indeed 
       parenthesis meta k peano imply parenthesis parenthesis meta k peano imply meta k end parenthesis peano imply meta k end parenthesis end parenthesis 
         peano imply 
       parenthesis parenthesis meta k peano imply parenthesis meta k peano imply meta k end parenthesis end parenthesis peano imply parenthesis meta k peano imply meta k end parenthesis end parenthesis
     end line
     line ell b because axiom prime a one indeed 
       meta k peano imply parenthesis parenthesis meta k peano imply meta k end parenthesis peano imply meta k end parenthesis
     end line
     line ell c because rule prime mp modus ponens ell a modus ponens ell b indeed 
       parenthesis meta k peano imply parenthesis meta k peano imply meta k end parenthesis end parenthesis
         peano imply
       parenthesis meta k peano imply meta k end parenthesis
     end line
     line ell d because axiom prime a one indeed
       meta k peano imply parenthesis meta k peano imply meta k end parenthesis
     end line
     because rule prime mp modus ponens ell c modus ponens ell d indeed 
       meta k peano imply meta k 
     qed
   end math ]"



\subsection{Corollary "[ math corollary one point ten a end math ]"}

"[ intro corollary one point ten a
   index "C1.10a"
   pyk   "corollary one point ten a"
   tex   "C1.10a"
   end intro ]"
\display{"[ math
  in theory system prime s
   lemma
     corollary one point ten a
   says
     all meta e indeed all meta k indeed all meta h indeed
     parenthesis
     meta e peano imply meta k 
       infer
     meta k peano imply meta h
       infer
     meta e peano imply meta h
     end parenthesis
   end lemma
  end math
]"}

"[ 
  math system prime s
   proof of
     corollary one point ten a
   reads
     arbitrary meta e end line
     arbitrary meta k end line
     arbitrary meta h end line
     line ell a premise 
       meta e peano imply meta k
     end line
     line ell b premise
       meta k peano imply meta h
     end line
     line ell c because axiom prime a one indeed
       parenthesis meta k peano imply meta h end parenthesis
       peano imply
       parenthesis
         meta e peano imply parenthesis meta k peano imply meta h end parenthesis
       end parenthesis
     end line
     line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
       meta e peano imply parenthesis meta k peano imply meta h end parenthesis
     end line
     line ell e because axiom prime a two indeed
       parenthesis meta e peano imply parenthesis meta k peano imply meta h end parenthesis end parenthesis
       peano imply
       parenthesis
         parenthesis meta e peano imply meta k end parenthesis
         peano imply
         parenthesis meta e peano imply meta h end parenthesis 
       end parenthesis
     end line
     line ell f because rule prime mp modus ponens ell e modus ponens ell d indeed
       parenthesis meta e peano imply meta k end parenthesis
       peano imply
       parenthesis meta e peano imply meta h end parenthesis
     end line
     because rule prime mp modus ponens ell f modus ponens ell a indeed
       meta e peano imply meta h 
     qed
   end math 
]"


\subsection{Corollary "[ math corollary one point ten b end math ]"}
"[ intro corollary one point ten b
   index "corollary one point ten b"
   pyk   "corollary one point ten b"
   tex   "C1.10b"
end intro ]"
\display{"[ math
  in theory system prime s lemma corollary one point ten b
  says
  all meta e indeed all meta k indeed all meta h indeed
  parenthesis
  meta e peano imply parenthesis meta k peano imply meta h end parenthesis
  infer meta k
  infer meta e peano imply meta h
  end parenthesis
  end lemma
  end math
]"}

"[
math system prime s
  proof of
    corollary one point ten b
  reads
     arbitrary meta e end line
     arbitrary meta k end line
     arbitrary meta h end line
     line ell a premise 
       meta e peano imply parenthesis meta k peano imply meta h end parenthesis
     end line
     line ell b premise
       meta k 
     end line
     line ell c because axiom prime a one indeed
       meta k peano imply parenthesis meta e peano imply meta k end parenthesis
     end line
     line ell d because rule prime mp modus ponens ell c modus ponens ell b indeed
       meta e peano imply meta k
     end line
     line ell e because axiom prime a two indeed
       parenthesis
         meta e peano imply parenthesis meta k peano imply meta h end parenthesis 
       end parenthesis
       peano imply
       parenthesis
         parenthesis meta e peano imply meta k end parenthesis
         peano imply
         parenthesis meta e peano imply meta h end parenthesis
       end parenthesis
     end line
     line ell f because rule prime mp modus ponens ell e modus ponens ell a indeed
       parenthesis meta e peano imply meta k end parenthesis
       peano imply
       parenthesis meta e peano imply meta h end parenthesis
     end line
     because rule prime mp modus ponens ell f modus ponens ell d indeed
       meta e peano imply meta h 
     qed
end math
]"



\subsection{Lemma "[ math lemma prime l three two b end math ]"}
To avoid variable clash we prove 
"[ intro lemma prime l three two b 
   index "L3.2(b)'"
   pyk "lemma prime l three two b"
   tex "L3.2(b)'"
   end intro ]"
using 
"[ intro lemma prime l three two b tmp
   index "\hat{L}3.2(b)'"
   pyk "lemma prime l three two b tmp"
   tex "\hat{L}3.2(b)'"
   end intro ]"

\display{"[ 
  math in theory system prime s lemma lemma prime l three two b tmp
  says 
    all meta t indeed
    all meta r indeed
    meta t peano is meta r peano imply meta r peano is meta t 
  end lemma end math 
]"}

"[
math system prime s
  proof of 
    lemma prime l three two b tmp
  reads
    arbitrary meta t end line
    arbitrary meta r end line
    line ell a because axiom prime s one indeed
      meta t peano is meta r 
      peano imply
      parenthesis
       meta t peano is meta t
        peano imply
       meta r peano is meta t
      end parenthesis
    end line
    line ell b because lemma prime l three two a indeed
      meta t peano is meta t
    end line
    because corollary one point ten b modus ponens ell a modus ponens ell b indeed
      meta t peano is meta r 
      peano imply 
      meta r peano is meta t
    qed
end math
]"

\display{"[ 
  math in theory system prime s 
  lemma 
    lemma prime l three two b
  says 
    all meta e indeed
    all meta f indeed
    parenthesis
      meta e peano is meta f peano imply meta f peano is meta e 
    end parenthesis
  end lemma end math 
]"}

"[
math system prime s
  proof of 
    lemma prime l three two b
  reads
    arbitrary meta e end line
    arbitrary meta f end line
    because lemma prime l three two b tmp indeed
      parenthesis
        meta e peano is meta f peano imply meta f peano is meta e 
      end parenthesis
    qed 
end math
]"



\subsection{Lemma "[ math lemma prime l three two c end math ]"}
To avoid variable clash we prove 
"[
intro lemma prime l three two c
 index "L3.2(c)'"
 pyk   "lemma prime l three two c"
 tex   "L3.2(c)'"
end intro
]"
using 
"[ 
intro lemma prime l three two c tmp
  index "\hat{L}3.2(c)'"
  pyk   "lemma prime l three two c tmp"
  tex   "\hat{L}3.2(c)'"
end intro
]"

\display{"[
math 
 in theory system prime s
  lemma
   lemma prime l three two c tmp
  says
   all meta t indeed
   all meta r indeed
   all meta s indeed
   meta t peano is meta r
     peano imply
   parenthesis
     meta r peano is meta s peano imply meta t peano is meta s
   end parenthesis
  end lemma
end math
]"}


"[
math system prime s
  proof of
    lemma prime l three two c tmp
  reads
    arbitrary meta t end line
    arbitrary meta r end line
    arbitrary meta s end line
    line ell a because axiom prime s one indeed
      meta r peano is meta t
      peano imply
      parenthesis
        meta r peano is meta s peano imply meta t peano is meta s
      end parenthesis
    end line
    line ell b because lemma prime l three two b indeed 
      meta t peano is meta r peano imply meta r peano is meta t
    end line
    because corollary one point ten a modus ponens ell b modus ponens ell a indeed
      meta t peano is meta r
      peano imply
      parenthesis
        meta r peano is meta s peano imply meta t peano is meta s
      end parenthesis
    qed 
end math
]"

\display{"[
math 
 in theory system prime s
  lemma
   lemma prime l three two c
  says
   all meta e indeed
   all meta f indeed
   all meta g indeed
   meta e peano is meta f
     peano imply
   parenthesis
     meta f peano is meta g peano imply meta e peano is meta g
   end parenthesis
  end lemma
end math
]"}

"[
math system prime s
  proof of
    lemma prime l three two c
  reads
    arbitrary meta e end line
    arbitrary meta f end line
    arbitrary meta g end line
    because lemma prime l three two c tmp indeed
      meta e peano is meta f
        peano imply
      parenthesis
        meta f peano is meta g peano imply meta e peano is meta g
      end parenthesis
    qed 
end math
]"


\subsection{Lemma "[ math tautology one end math ]"}
"[
intro tautology one
  index "Tautology 1"
  pyk   "tautology one"
  tex   "Tautology 1"
end intro
]"

\display{"[ math 
  in theory system prime s lemma tautology one 
    says 
      all meta e indeed
      all meta f indeed
      all meta g indeed
      parenthesis
        parenthesis 
          meta e peano imply parenthesis meta f peano imply meta g end parenthesis 
        end parenthesis 
        infer
        parenthesis 
          meta f peano imply parenthesis meta e peano imply meta g end parenthesis 
        end parenthesis
      end parenthesis
    end lemma 
  end math 
]"}

"[
math system prime s
  proof of
    tautology one
  reads
  arbitrary meta e end line
  arbitrary meta f end line
  arbitrary meta g end line
  line ell a premise 
    meta e peano imply parenthesis meta f peano imply meta g end parenthesis 
  end line
  line ell b because axiom prime a two indeed 
    parenthesis
      meta e peano imply parenthesis meta f peano imply meta g end parenthesis
    end parenthesis
    peano imply
    parenthesis
      parenthesis meta e peano imply meta f end parenthesis
      peano imply
      parenthesis meta e peano imply meta g end parenthesis
    end parenthesis
  end line
  line ell c because rule prime mp modus ponens ell b modus ponens ell a indeed
    parenthesis meta e peano imply meta f end parenthesis
    peano imply 
    parenthesis meta e peano imply meta g end parenthesis
  end line
  line ell d because axiom prime a one indeed
    parenthesis 
      parenthesis meta e peano imply meta f end parenthesis
      peano imply 
      parenthesis meta e peano imply meta g end parenthesis
    end parenthesis
    peano imply
    parenthesis
      meta f
      peano imply
      parenthesis
        parenthesis
          meta e peano imply meta f
        end parenthesis
        peano imply
        parenthesis
          meta e peano imply meta g
        end parenthesis
      end parenthesis
    end parenthesis
  end line
  line ell e because rule prime mp modus ponens ell d modus ponens ell c indeed
    meta f
    peano imply
    parenthesis
      parenthesis
        meta e peano imply meta f
      end parenthesis
      peano imply
      parenthesis
        meta e peano imply meta g
      end parenthesis
    end parenthesis
  end line
  line ell f because axiom prime a two indeed
    parenthesis
    meta f
    peano imply
    parenthesis
      parenthesis
        meta e peano imply meta f
      end parenthesis
      peano imply
      parenthesis
        meta e peano imply meta g
      end parenthesis
    end parenthesis
    end parenthesis
    peano imply
    parenthesis
      parenthesis
        meta f
        peano imply
          parenthesis
            meta e peano imply meta f
          end parenthesis
        end parenthesis
      peano imply
      parenthesis
        meta f
        peano imply
          parenthesis
            meta e peano imply meta g
          end parenthesis
      end parenthesis
    end parenthesis
  end line
  line ell g because rule prime mp modus ponens ell f modus ponens ell e indeed 
    parenthesis
      meta f
      peano imply
        parenthesis
          meta e peano imply meta f
        end parenthesis
      end parenthesis
    peano imply
    parenthesis
      meta f
      peano imply
        parenthesis
          meta e peano imply meta g
        end parenthesis
    end parenthesis
  end line
  line ell h because axiom prime a one indeed 
    meta f 
    peano imply 
    parenthesis meta e peano imply meta f end parenthesis
  end line
  because rule prime mp modus ponens ell g modus ponens ell h indeed
    meta f
    peano imply
    parenthesis meta e peano imply meta g end parenthesis
  qed

end math
]"



\subsection{Lemma "[ math lemma prime l three two d end math ]"}
To avoid variable clash we prove
"[
intro lemma prime l three two d
  index "L3.2(d)'"
  pyk   "lemma prime l three two d"
  tex   "L3.2(d)'"
end intro
]"
using 
"[
intro lemma prime l three two d tmp
  index "\hat{L}3.2(d)'"
  pyk   "lemma prime l three two d tmp"
  tex   "\hat{L}3.2(d)'"
end intro
]"


\display{"[ math 
in theory system prime s
  lemma
    lemma prime l three two d tmp
  says
  all meta t indeed
  all meta r indeed
  all meta s indeed
  meta r peano is meta t
  peano imply
    parenthesis
      meta s peano is meta t
      peano imply
      meta r peano is meta s
    end parenthesis
  end lemma
end math
]"}

"[ math 
system prime s
  proof of  
    lemma prime l three two d tmp
  reads
    arbitrary meta t end line
    arbitrary meta r end line
    arbitrary meta s end line
    line ell a because lemma prime l three two c indeed
      meta r peano is  meta t
      peano imply
      parenthesis
        meta t peano is meta s
        peano imply
        meta r peano is meta s
      end parenthesis
    end line
    line ell b because tautology one modus ponens ell a indeed
      meta t peano is meta s
      peano imply
      parenthesis
        meta r peano is  meta t
        peano imply
        meta r peano is meta s
      end parenthesis
    end line 
    line ell c because lemma prime l three two b indeed
      meta s peano is meta t peano imply meta t peano is meta s
    end line
    line ell d because corollary one point ten a modus ponens ell c modus ponens ell b indeed
      meta s peano is meta t
      peano imply
      parenthesis
        meta r peano is  meta t
        peano imply
        meta r peano is meta s
      end parenthesis
    end line
    because tautology one modus ponens ell d indeed
      meta r peano is  meta t
      peano imply
      parenthesis
        meta s peano is meta t
        peano imply
        meta r peano is meta s
      end parenthesis
    qed 
end math
]"

\display{"[ math 
in theory system prime s
  lemma
    lemma prime l three two d
  says
  all meta e indeed
  all meta f indeed
  all meta g indeed
  meta f peano is meta e
  peano imply
    parenthesis
      meta g peano is meta e
      peano imply
      meta f peano is meta g
    end parenthesis
  end lemma
end math
]"}

"[ math 
system prime s
  proof of  
    lemma prime l three two d
  reads
    arbitrary meta e end line
    arbitrary meta f end line
    arbitrary meta g end line
    because lemma prime l three two d tmp indeed
      meta f peano is meta e
        peano imply
      parenthesis
        meta g peano is meta e
        peano imply
        meta f peano is meta g
      end parenthesis      
    qed
end math
]"


\clearpage

\appendix

\section{Chores}

\subsection{The name of the page}

This defines the name of the page:

\display{"[ math pyk define logik rapport as "logik rapport" end define end math ]"}



\subsection{\TeX\ definitions}\label{section:TexDefinitions}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outex
\input{./page.otx}
\item \mbox{}
\end{list}



\subsection{Test}

\begin{list}{}{
\setlength{\leftmargin}{5em}
\setlength{\itemindent}{-5em}}
\immediate\closeout\outest
\input{./page.tst}
\item \mbox{}
\end{list}



\subsection{Priority table}\label{section:PriorityTable}


"[ flush left math priority table Priority end table end math end left ]"



\section{Index}

\newcommand\myidxitem{\par\noindent}

\renewenvironment{theindex}{\let\item\myidxitem}{}

\printindex



\section{Bibliography}

\bibliography{./page}

\end{document}
End of file
File page.bib

@article      {berline97,
  author    = {C. Berline and K. Grue},
  title     = {A $\kappa$-denotational semantics for {M}ap {T}heory
               in {ZFC+SI}},
  journal   = TCS,
  year      = {1997},
  volume    = {179},
  number    = {1--2},
  pages     = {137--202},
  month     = {jun}}

@book         {church41,
  author    = {A. Church},
  title     = {The Calculi of Lambda-Conversion},
  publisher = {Princeton University Press},
  year      = {1941}}

@Article      {godel,
  author    = {K. G{\"!o}del},
  title     = {{\"!U}ber for\-mal un\-ent\-scheid\-ba\-re
               \mbox{S\"!at}\-ze der \mbox{Prin}\-ci\-pia 
               \mbox{Mathe}\-ma\-ti\-ca und ver\-wand\-ter
               \mbox{Sys}\-teme \mbox{I}},
  journal   = {Mo\-nats\-hef\-te f{\"!u}r Mathe\-ma\-tik und Phy\-sik},
  year      = {19\-31},
  volume    = {12},
  number    = {\mbox{XXXVIII}},
  pages     = {173-198}}

@book         {Gordon79,
  author    = {M. J. Gordon, A. J. Milner, C. P. Wadsworth},
  title     = {Edinburgh {LCF}, A mechanised logic of computation},
  publisher = {Springer-Verlag},
  year      = {1979},
  volume    = {78},
  series    = {Lecture Notes in Computer Science}}

@article      {grue92,
  author    = {K. Grue},
  title     = {Map Theory},
  journal   = TCS,
  year      = {1992},
  volume    = {102},
  number    = {1},
  pages     = {1--133},
  month     = {jul}}

@inproceedings{Logiweb,
  author    = {K. Grue},
  title     = {Logiweb},
  editor    = {Fairouz Kamareddine},
  booktitle = {Mathematical Knowledge Management Symposium 2003},
  publisher = {Elsevier},
  series    = {Electronic Notes in Theoretical Computer Science},
  volume    = {93},
  year      = {2004},
  pages     = {70--101}}

@article      {mccarthy60,
   author   = {J. McCarthy},
   title    = {Recursive functions of symbolic expressions and their 
               computation by machine},
   journal  = {Communications of the ACM},
   year     = {1960},
   pages    = {184--195}}

@book         {mendelson,
  author =    {E. Mendelson},
  title =     {Introduction to Mathematical Logic},
  publisher = {Wadsworth and Brooks},
  year =      {1987},
  edition =   {3.}}

@book         {TeXbook,
  author    = {D. Knuth},
  title     = {The TeXbook},
  publisher = {Addison Wesley},
  year      = {1983}}

End of file
File page.sty
% thebibliography environment from
% /usr/share/texmf/tex/latex/base/book.cls
% with \chapter removed
\renewenvironment{thebibliography}[1]
     {\list{\@biblabel{\@arabic\c at enumiv}}%
           {\settowidth\labelwidth{\@biblabel{#1}}%
            \leftmargin\labelwidth
            \advance\leftmargin\labelsep
            \@openbib at code
            \usecounter{enumiv}%
            \let\p at enumiv\@empty
            \renewcommand\theenumiv{\@arabic\c at enumiv}}%
      \sloppy
      \clubpenalty4000
      \@clubpenalty \clubpenalty
      \widowpenalty4000%
      \sfcode`\.\@m}
     {\def\@noitemerr
       {\@latex at warning{Empty `thebibliography' environment}}%
      \endlist}
End of file
latex page
makeindex page
bibtex page
latex page
makeindex page
latex page"


More information about the Logiweb mailing list