berghofe@3098: \documentclass[12pt]{report}
paulson@3128: \usepackage{a4,proof}
berghofe@3098: 
wenzelm@2657: \makeatletter
wenzelm@2659: \input{../rail.sty}
wenzelm@2657: \input{../iman.sty}
wenzelm@2657: \input{../extra.sty}
wenzelm@2657: \makeatother
wenzelm@2657: 
lcp@104: %% $Id$
lcp@349: %%\includeonly{}
lcp@104: %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}
lcp@104: %%% to delete old ones:  \\indexbold{\*[^}]*}
lcp@104: %% run    sedindex ref    to prepare index file
lcp@104: %%% needs chapter on Provers/typedsimp.ML?
lcp@104: \title{The Isabelle Reference Manual}
lcp@104: 
paulson@3128: \author{{\em Lawrence C. Paulson}\\
paulson@3128:         Computer Laboratory \\ University of Cambridge \\
paulson@3128:         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 
paulson@3128:         With Contributions by Tobias Nipkow and Markus Wenzel%
lcp@349: \thanks{Tobias Nipkow, of T. U. Munich, wrote most of
lcp@349:   Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, and part of
lcp@349:   Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to
lcp@349:   Chapter~\protect\ref{theories}.  Markus Wenzel contributed to
paulson@1877:   Chapter~\protect\ref{chap:syntax}.  Sara Kalvala, Martin Simons and others
paulson@1877:   suggested changes
paulson@3128:   and corrections.  The research has been funded by the EPSRC (grants
paulson@3128:   GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453:
paulson@3128:   Types.}} 
lcp@349: 
lcp@104: \makeindex
lcp@104: 
lcp@104: \setcounter{secnumdepth}{1} \setcounter{tocdepth}{2}
lcp@104: 
lcp@104: \pagestyle{headings}
lcp@104: \sloppy
lcp@104: \binperiod     %%%treat . like a binary operator
lcp@104: 
wenzelm@3108: \railalias{lbrace}{\ttlbrace}
wenzelm@3108: \railalias{rbrace}{\ttrbrace}
berghofe@3098: \railterm{lbrace,rbrace}
berghofe@3098: 
lcp@104: \begin{document}
wenzelm@3108: \underscoreoff
wenzelm@3108: 
lcp@104: \index{definitions|see{rewriting, meta-level}}
lcp@104: \index{rewriting!object-level|see{simplification}}
lcp@323: \index{meta-rules|see{meta-rules}}
lcp@286: 
lcp@286: \maketitle 
lcp@286: \pagenumbering{roman} \tableofcontents \clearfirst
lcp@286: 
lcp@104: \include{introduction}
lcp@104: \include{goals}
lcp@104: \include{tactic}
lcp@104: \include{tctical}
lcp@104: \include{thm}
lcp@104: \include{theories}
lcp@323: \include{defining}
lcp@323: \include{syntax}
lcp@104: \include{substitution}
lcp@104: \include{simplifier}
lcp@104: \include{classical}
lcp@104: 
lcp@104: %%seealso's must be last so that they appear last in the index entries
lcp@323: \index{meta-rewriting|seealso{tactics, theorems}}
lcp@104: 
lcp@286: \begingroup
lcp@286:   \bibliographystyle{plain} \small\raggedright\frenchspacing
lcp@873:   \bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref}
lcp@286: \endgroup
nipkow@302: \include{theory-syntax}
lcp@349: 
lcp@349: \input{ref.ind}
lcp@104: \end{document}