author  paulson 
Wed, 07 Oct 1998 10:31:30 +0200  
changeset 5619  76a8c72e3fd4 
parent 5170  33fbffd06c12 
child 6568  b38bc78d9a9d 
permissions  rwrr 
3098  1 
\documentclass[12pt]{report} 
5165  2 
\usepackage{graphicx,a4,../iman,../extra,../proof,../rail,../pdfsetup} 
2657  3 

104  4 
%% $Id$ 
349  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? 

5170  10 
\title{\includegraphics[scale=0.5]{isabelle.eps} \\[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 

1877  21 
Chapter~\protect\ref{chap:syntax}. Sara Kalvala, Martin Simons and others 
22 
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 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

24 
GR/G53279, GR/H40570, GR/K57381, GR/K77051) and by ESPRIT project 6453: 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

25 
Types.}} 
349  26 

104  27 
\makeindex 
28 

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

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

31 
\pagestyle{headings} 

32 
\sloppy 

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

34 

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

3098  37 
\railterm{lbrace,rbrace} 
38 

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

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

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

46 
\maketitle 

47 
\pagenumbering{roman} \tableofcontents \clearfirst 

48 

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

51 
\include{tactic} 

52 
\include{tctical} 

53 
\include{thm} 

54 
\include{theories} 

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

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

59 
\include{classical} 

60 

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

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

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

873  66 
\bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref} 
286  67 
\endgroup 
302  68 
\include{theorysyntax} 
349  69 

70 
\input{ref.ind} 

104  71 
\end{document} 