doc-src/Ref/ref.tex
changeset 286 e7efbf03562b
parent 183 f34acf216a32
child 302 7e2cffe28eb5
equal deleted inserted replaced
285:fd4a6585e5bf 286:e7efbf03562b
     1 \documentstyle[a4,12pt,proof,iman,alltt]{report}
     1 \documentstyle[a4,12pt,proof,iman,extra]{report}
     2 %% $Id$
     2 %% $Id$
     3 %%% \includeonly{thm}
     3 %%% \includeonly{thm}
     4 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
     4 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
     5 %%% to delete old ones:  \\indexbold{\*[^}]*}
     5 %%% to delete old ones:  \\indexbold{\*[^}]*}
     6 %% run    sedindex ref    to prepare index file
     6 %% run    sedindex ref    to prepare index file
    10 \author{{\em Lawrence C. Paulson}\thanks
    10 \author{{\em Lawrence C. Paulson}\thanks
    11 {Tobias Nipkow, of T. U. Munich, wrote Chapter~8 and part of Chapter~6.
    11 {Tobias Nipkow, of T. U. Munich, wrote Chapter~8 and part of Chapter~6.
    12  Carsten Clasohm also contributed to Chapter~6.
    12  Carsten Clasohm also contributed to Chapter~6.
    13  Sara Kalvala and Markus Wenzel suggested changes and corrections.
    13  Sara Kalvala and Markus Wenzel suggested changes and corrections.
    14  The research has been funded by the SERC (grants GR/G53279, GR/H40570)
    14  The research has been funded by the SERC (grants GR/G53279, GR/H40570)
    15   and by ESPRIT project 6453: Types).} 
    15   and by ESPRIT project 6453: Types.} 
    16 \\  
    16 \\  
    17         Computer Laboratory \\ University of Cambridge \\[2ex]
    17         Computer Laboratory \\ University of Cambridge \\[2ex]
    18         {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
    18         {\small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}} \\[3cm]
    19     {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
    19     {\small Copyright \copyright{} \number\year{} by Lawrence C. Paulson}
    20 }
    20 }
    31 
    31 
    32 \begin{document}
    32 \begin{document}
    33 \index{definitions|see{rewriting, meta-level}}
    33 \index{definitions|see{rewriting, meta-level}}
    34 \index{rewriting!object-level|see{simplification}}
    34 \index{rewriting!object-level|see{simplification}}
    35 \index{rules!meta-level|see{meta-rules}}
    35 \index{rules!meta-level|see{meta-rules}}
       
    36 
       
    37 \maketitle 
       
    38 \pagenumbering{roman} \tableofcontents \clearfirst
       
    39 
    36 \include{introduction}
    40 \include{introduction}
    37 \include{goals}
    41 \include{goals}
    38 \include{tactic}
    42 \include{tactic}
    39 \include{tctical}
    43 \include{tctical}
    40 \include{thm}
    44 \include{thm}
    44 \include{classical}
    48 \include{classical}
    45 
    49 
    46 %%seealso's must be last so that they appear last in the index entries
    50 %%seealso's must be last so that they appear last in the index entries
    47 \index{rewriting!meta-level|seealso{tactics, theorems}}
    51 \index{rewriting!meta-level|seealso{tactics, theorems}}
    48 
    52 
    49 \bibliographystyle{plain} \small\raggedright\frenchspacing
    53 \begingroup
    50 \bibliography{atp,funprog,general,logicprog,theory}
    54   \bibliographystyle{plain} \small\raggedright\frenchspacing
    51 \input{ref.ind}
    55   \bibliography{atp,funprog,general,logicprog,theory}
       
    56 \endgroup
       
    57 \include{Ref/theory-syntax}
       
    58 \addcontentsline{toc}{chapter}{Index}\input{ref.ind}
    52 \end{document}
    59 \end{document}