author  paulson 
Wed, 07 May 1997 16:29:06 +0200  
changeset 3128  d01d4c0c4b44 
parent 3108  335efc3f5632 
child 3223  49f1a09576c2 
permissions  rwrr 
3098  1 
\documentclass[12pt]{report} 
3128
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

2 
\usepackage{a4,proof} 
3098  3 

2657  4 
\makeatletter 
2659  5 
\input{../rail.sty} 
2657  6 
\input{../iman.sty} 
7 
\input{../extra.sty} 

8 
\makeatother 

9 

104  10 
%% $Id$ 
349  11 
%%\includeonly{} 
104  12 
%%% to index ids: \[\\tt \([azAZ09][azAZ09_'.]*\) [\\ttindexbold{\1} 
13 
%%% to delete old ones: \\indexbold{\*[^}]*} 

14 
%% run sedindex ref to prepare index file 

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

16 
\title{The Isabelle Reference Manual} 

17 

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

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

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

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

21 
With Contributions by Tobias Nipkow and Markus Wenzel% 
349  22 
\thanks{Tobias Nipkow, of T. U. Munich, wrote most of 
23 
Chapters~\protect\ref{DefiningLogics} and~\protect\ref{simpchap}, and part of 

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

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

1877  26 
Chapter~\protect\ref{chap:syntax}. Sara Kalvala, Martin Simons and others 
27 
suggested changes 

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

28 
and corrections. The research has been funded by the EPSRC (grants 
d01d4c0c4b44
New acknowledgements; fixed overfull lines and tables
paulson
parents:
3108
diff
changeset

29 
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

30 
Types.}} 
349  31 

104  32 
\makeindex 
33 

34 
\setcounter{secnumdepth}{1} \setcounter{tocdepth}{2} 

35 

36 
\pagestyle{headings} 

37 
\sloppy 

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

39 

3108  40 
\railalias{lbrace}{\ttlbrace} 
41 
\railalias{rbrace}{\ttrbrace} 

3098  42 
\railterm{lbrace,rbrace} 
43 

104  44 
\begin{document} 
3108  45 
\underscoreoff 
46 

104  47 
\index{definitionssee{rewriting, metalevel}} 
48 
\index{rewriting!objectlevelsee{simplification}} 

323  49 
\index{metarulessee{metarules}} 
286  50 

51 
\maketitle 

52 
\pagenumbering{roman} \tableofcontents \clearfirst 

53 

104  54 
\include{introduction} 
55 
\include{goals} 

56 
\include{tactic} 

57 
\include{tctical} 

58 
\include{thm} 

59 
\include{theories} 

323  60 
\include{defining} 
61 
\include{syntax} 

104  62 
\include{substitution} 
63 
\include{simplifier} 

64 
\include{classical} 

65 

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

323  67 
\index{metarewritingseealso{tactics, theorems}} 
104  68 

286  69 
\begingroup 
70 
\bibliographystyle{plain} \small\raggedright\frenchspacing 

873  71 
\bibliography{string,atp,funprog,general,logicprog,isabelle,theory,crossref} 
286  72 
\endgroup 
302  73 
\include{theorysyntax} 
349  74 

75 
\input{ref.ind} 

104  76 
\end{document} 