author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 9695  ec7d7f877712 
child 14149  fac076f0c71c 
permissions  rwrr 
7838  1 
\documentclass[12pt,a4paper]{report} 
9695  2 
\usepackage{graphicx,../iman,../extra,../ttbox,../proof,../rail,../pdfsetup} 
2657  3 

104  4 
%% $Id$ 
6572  5 
%%\includeonly{} 
104  6 
%%% to index ids: \[\\tt \([azAZ09][azAZ09_'.]*\) [\\ttindexbold{\1} 
7 
%%% to delete old ones: \\indexbold{\*[^}]*} 

8 
%% run sedindex ref to prepare index file 

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

6571  10 
\title{\includegraphics[scale=0.5]{isabelle} \\[4ex] The Isabelle Reference Manual} 
104  11 

3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

12 
\author{{\em Lawrence C. Paulson}\\ 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

13 
Computer Laboratory \\ University of Cambridge \\ 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

14 
\texttt{lcp@cl.cam.ac.uk}\\[3ex] 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

15 
With Contributions by Tobias Nipkow and Markus Wenzel% 
349  16 
\thanks{Tobias Nipkow, of T. U. Munich, wrote most of 
3950  17 
Chapters~\protect\ref{DefiningLogics} and~\protect\ref{chap:simplification}, 
18 
and part of 

349  19 
Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to 
20 
Chapter~\protect\ref{theories}. Markus Wenzel contributed to 

8979  21 
Chapter~\protect\ref{chap:syntax}. Jeremy Dawson, Sara Kalvala, Martin 
22 
Simons and others suggested changes 

3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

23 
and corrections. The research has been funded by the EPSRC (grants 
8979  24 
GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT 
25 
(projects 3245: Logical Frameworks, and 6453: Types), and by the DFG 

26 
Schwerpunktprogramm \emph{Deduktion}.}} 

349  27 

104  28 
\makeindex 
29 

3223
49f1a09576c2
Section numbers may now be nested three deep, as in 1.2.3
paulson
parents:
3128
diff
changeset

30 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 
104  31 

32 
\pagestyle{headings} 

33 
\sloppy 

34 
\binperiod %%%treat . like a binary operator 

35 

3108  36 
\railalias{lbrace}{\ttlbrace} 
37 
\railalias{rbrace}{\ttrbrace} 

3098  38 
\railterm{lbrace,rbrace} 
39 

104  40 
\begin{document} 
3108  41 
\underscoreoff 
42 

104  43 
\index{definitionssee{rewriting, metalevel}} 
44 
\index{rewriting!objectlevelsee{simplification}} 

323  45 
\index{metarulessee{metarules}} 
286  46 

47 
\maketitle 

48 
\pagenumbering{roman} \tableofcontents \clearfirst 

49 

104  50 
\include{introduction} 
51 
\include{goals} 

52 
\include{tactic} 

53 
\include{tctical} 

54 
\include{thm} 

55 
\include{theories} 

323  56 
\include{defining} 
57 
\include{syntax} 

104  58 
\include{substitution} 
59 
\include{simplifier} 

60 
\include{classical} 

61 

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

323  63 
\index{metarewritingseealso{tactics, theorems}} 
104  64 

286  65 
\begingroup 
66 
\bibliographystyle{plain} \small\raggedright\frenchspacing 

6592  67 
\bibliography{../manual} 
286  68 
\endgroup 
302  69 
\include{theorysyntax} 
349  70 

8828  71 
\printindex 
104  72 
\end{document} 