author  obua 
Fri, 16 Sep 2005 21:02:15 +0200  
changeset 17440  df77edc4f5d0 
parent 14149  fac076f0c71c 
child 30118  df610709eda5 
child 30240  5b25fee0362c 
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] 
14149
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

15 
With Contributions by Tobias Nipkow and Markus Wenzel} 
349  16 

104  17 
\makeindex 
18 

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

19 
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2} 
104  20 

21 
\pagestyle{headings} 

22 
\sloppy 

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

24 

3108  25 
\railalias{lbrace}{\ttlbrace} 
26 
\railalias{rbrace}{\ttrbrace} 

3098  27 
\railterm{lbrace,rbrace} 
28 

104  29 
\begin{document} 
3108  30 
\underscoreoff 
31 

104  32 
\index{definitionssee{rewriting, metalevel}} 
33 
\index{rewriting!objectlevelsee{simplification}} 

323  34 
\index{metarulessee{metarules}} 
286  35 

36 
\maketitle 

14149
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

37 
\emph{Note}: this document is part of the earlier Isabelle documentation, 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

38 
which is somewhat superseded by the Isabelle/HOL 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

39 
\emph{Tutorial}~\cite{isatutorial}. Much of it is concerned with 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

40 
the oldstyle theory syntax and the primitives for conducting proofs 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

41 
using the ML top level. This style of interaction is largely obsolete: 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

42 
most Isabelle proofs are now written using the Isar 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

43 
language and the Proof General interface. However, this is the only 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

44 
comprehensive Isabelle reference manual. 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

45 

fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

46 
See also the \emph{Introduction to Isabelle}, which has tutorial examples 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

47 
on conducting proofs using the ML toplevel. 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

48 

fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

49 
\subsubsection*{Acknowledgements} 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

50 
Tobias Nipkow, of T. U. Munich, wrote most of 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

51 
Chapters~\protect\ref{DefiningLogics} and~\protect\ref{chap:simplification}, 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

52 
and part of 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

53 
Chapter~\protect\ref{theories}. Carsten Clasohm also contributed to 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

54 
Chapter~\protect\ref{theories}. Markus Wenzel contributed to 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

55 
Chapter~\protect\ref{chap:syntax}. Jeremy Dawson, Sara Kalvala, Martin 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

56 
Simons and others suggested changes 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

57 
and corrections. The research has been funded by the EPSRC (grants 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

58 
GR/G53279, GR/H40570, GR/K57381, GR/K77051, GR/M75440) and by ESPRIT 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

59 
(projects 3245: Logical Frameworks, and 6453: Types), and by the DFG 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

60 
Schwerpunktprogramm \emph{Deduktion}. 
fac076f0c71c
reformatting change and mention of Introduction to Isabelle
paulson
parents:
9695
diff
changeset

61 

286  62 
\pagenumbering{roman} \tableofcontents \clearfirst 
63 

104  64 
\include{introduction} 
65 
\include{goals} 

66 
\include{tactic} 

67 
\include{tctical} 

68 
\include{thm} 

69 
\include{theories} 

323  70 
\include{defining} 
71 
\include{syntax} 

104  72 
\include{substitution} 
73 
\include{simplifier} 

74 
\include{classical} 

75 

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

323  77 
\index{metarewritingseealso{tactics, theorems}} 
104  78 

286  79 
\begingroup 
80 
\bibliographystyle{plain} \small\raggedright\frenchspacing 

6592  81 
\bibliography{../manual} 
286  82 
\endgroup 
302  83 
\include{theorysyntax} 
349  84 

8828  85 
\printindex 
104  86 
\end{document} 