1 \documentclass[12pt,a4paper]{report}
2 \usepackage{graphicx,../iman,../extra,../proof,../rail,../pdfsetup}
6 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\) [\\ttindexbold{\1}
7 %%% to delete old ones: \\indexbold{\*[^}]*}
8 %% run sedindex ref to prepare index file
9 %%% needs chapter on Provers/typedsimp.ML?
10 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual}
12 \author{{\em Lawrence C. Paulson}\\
13 Computer Laboratory \\ University of Cambridge \\
14 \texttt{lcp@cl.cam.ac.uk}\\[3ex]
15 With Contributions by Tobias Nipkow and Markus Wenzel%
16 \thanks{Tobias Nipkow, of T. U. Munich, wrote most of
17 Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},
19 Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to
20 Chapter~\protect\ref{theories}. Markus Wenzel contributed to
21 Chapter~\protect\ref{chap:syntax}. Sara Kalvala, Martin Simons and others
23 and corrections. The research has been funded by the EPSRC (grants
24 GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453:
29 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
33 \binperiod %%%treat . like a binary operator
35 \railalias{lbrace}{\ttlbrace}
36 \railalias{rbrace}{\ttrbrace}
37 \railterm{lbrace,rbrace}
42 \index{definitions|see{rewriting, meta-level}}
43 \index{rewriting!object-level|see{simplification}}
44 \index{meta-rules|see{meta-rules}}
47 \pagenumbering{roman} \tableofcontents \clearfirst
49 \include{introduction}
57 \include{substitution}
61 %%seealso's must be last so that they appear last in the index entries
62 \index{meta-rewriting|seealso{tactics, theorems}}
65 \bibliographystyle{plain} \small\raggedright\frenchspacing
66 \bibliography{../manual}
68 \include{theory-syntax}