author | lcp |
Wed, 19 Oct 1994 09:23:56 +0100 | |
changeset 642 | 0db578095e6a |
parent 349 | 0ddc495e8b83 |
child 873 | 0cfc734e3dbd |
permissions | -rw-r--r-- |
\documentstyle[a4,12pt,rail,proof,iman,extra]{report} %% $Id$ %%\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{The Isabelle Reference Manual} \author{{\em Lawrence C. Paulson}% \thanks{Tobias Nipkow, of T. U. Munich, wrote most of Chapters~\protect\ref{Defining-Logics} and~\protect\ref{simp-chap}, 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}. Sara Kalvala and others suggested changes and corrections. The research has been funded by the SERC (grants GR/G53279, GR/H40570) and by ESPRIT project 6453: Types.} \\ Computer Laboratory \\ University of Cambridge \\[2ex] \small{\em Electronic mail\/}: {\tt lcp@cl.cam.ac.uk}\\[3cm] Copyright \copyright{} \number\year{} by Lawrence C. Paulson} \date{} \makeindex \underscoreoff \setcounter{secnumdepth}{1} \setcounter{tocdepth}{2} \pagestyle{headings} \sloppy \binperiod %%%treat . like a binary operator \begin{document} \index{definitions|see{rewriting, meta-level}} \index{rewriting!object-level|see{simplification}} \index{meta-rules|see{meta-rules}} \maketitle \pagenumbering{roman} \tableofcontents \clearfirst \include{introduction} \include{goals} \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{string,atp,funprog,general,logicprog,isabelle,theory} \endgroup \include{theory-syntax} \input{ref.ind} \end{document}