\documentclass[12pt,a4paper]{report}

 \usepackage{graphicx,../iman,../extra,../ttbox,../proof,../pdfsetup}

 %%\includeonly{}

 %%% to index ids: \[\\tt \([a-zA-Z0-9][a-zA-Z0-9_'.]*\)    [\\ttindexbold{\1}

 %%% to delete old ones:  \\indexbold{\*[^}]*}

 %% run    sedindex ref    to prepare index file

 %%% needs chapter on Provers/typedsimp.ML?

 \title{\includegraphics[scale=0.5]{isabelle} \\[4ex] Old Isabelle Reference Manual}

 \author{{\em Lawrence C. Paulson}\\

         Computer Laboratory \\ University of Cambridge \\

         \texttt{lcp@cl.cam.ac.uk}\\[3ex] 

         With Contributions by Tobias Nipkow and Markus Wenzel}  

 \makeindex

 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

 \pagestyle{headings}

 \sloppy

 \binperiod     %%%treat . like a binary operator

 \begin{document}

 \underscoreoff

 \index{definitions|see{rewriting, meta-level}}

 \index{rewriting!object-level|see{simplification}}

 \index{meta-rules|see{meta-rules}}

 \maketitle 

 \emph{Note}: this document is part of the earlier Isabelle

 documentation and is mostly outdated.  Fully obsolete parts of the

 original text have already been removed.  The remaining material

 covers some aspects that did not make it into the newer manuals yet.

 \subsubsection*{Acknowledgements} 

 Tobias Nipkow, of T. U. Munich, wrote most of

   Chapters~\protect\ref{Defining-Logics} and~\protect\ref{chap:simplification},

   and part of

   Chapter~\protect\ref{theories}.  Carsten Clasohm also contributed to

   Chapter~\protect\ref{theories}.  Markus Wenzel contributed to

   Chapter~\protect\ref{chap:syntax}.  Jeremy Dawson, Sara Kalvala, Martin

   Simons  and others suggested changes

   and corrections.  The research has been funded by the EPSRC (grants

   GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT

   (projects 3245: Logical Frameworks, and 6453: Types), and by the DFG

   Schwerpunktprogramm \emph{Deduktion}.

 \pagenumbering{roman} \tableofcontents \clearfirst

 \include{introduction}

 \include{tactic}

 \include{tctical}

 \include{thm}

 \include{theories}

 \include{defining}

 \include{syntax}

 \include{substitution}

 \include{simplifier}

 \include{classical}

 %%seealso's must be last so that they appear last in the index entries

 \index{meta-rewriting|seealso{tactics, theorems}}

 \begingroup

   \bibliographystyle{plain} \small\raggedright\frenchspacing

   \bibliography{../manual}

 \endgroup

 \include{theory-syntax}

 \printindex

 \end{document}