41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover. 
41 Isabelle~\cite{paulson86,paulson89,paulson700} is a generic theorem prover. 
42 It has been instantiated to support reasoning in several objectlogics: 
42 It has been instantiated to support reasoning in several objectlogics: 
43 \begin{itemize} 
43 \begin{itemize} 
44 \item firstorder logic, constructive and classical versions 
44 \item firstorder logic, constructive and classical versions 
45 \item higherorder logic, similar to that of Gordon's {\sc 
45 \item higherorder logic, similar to that of Gordon's {\sc 
46 hol}~\cite{gordon88a} 
46 hol}~\cite{mgordonhol} 
47 \item ZermeloFraenkel set theory~\cite{suppes72} 
47 \item ZermeloFraenkel set theory~\cite{suppes72} 
48 \item an extensional version of MartinL\"of's Type Theory~\cite{nordstrom90} 
48 \item an extensional version of MartinL\"of's Type Theory~\cite{nordstrom90} 
49 \item the classical firstorder sequent calculus, {\sc lk} 
49 \item the classical firstorder sequent calculus, {\sc lk} 
50 \item the modal logics $T$, $S4$, and $S43$ 
50 \item the modal logics $T$, $S4$, and $S43$ 
51 \item the Logic for Computable Functions~\cite{paulson87} 
51 \item the Logic for Computable Functions~\cite{paulson87} 
66 including a simple theorem prover. Users must be familiar with logic as 
66 including a simple theorem prover. Users must be familiar with logic as 
67 used in computer science; there are many good 
67 used in computer science; there are many good 
68 texts~\cite{galton90,reeves90}. 
68 texts~\cite{galton90,reeves90}. 
69 
69 
70 \index{LCF} 
70 \index{LCF} 
71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{gordon79}, is an 
71 {\sc lcf}, developed by Robin Milner and colleagues~\cite{mgordon79}, is an 
72 ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows 
72 ancestor of {\sc hol}, Nuprl, and several other systems. Isabelle borrows 
73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an 
73 ideas from {\sc lcf}: formulae are~\ML{} values; theorems belong to an 
74 abstract type; tactics and tacticals support backward proof. But {\sc lcf} 
74 abstract type; tactics and tacticals support backward proof. But {\sc lcf} 
75 represents objectlevel rules by functions, while Isabelle represents them 
75 represents objectlevel rules by functions, while Isabelle represents them 
76 by terms. You may find my other writings~\cite{paulson87,paulsonhandbook} 
76 by terms. You may find my other writings~\cite{paulson87,paulsonhandbook} 
77 helpful in understanding the relationship between {\sc lcf} and Isabelle. 
77 helpful in understanding the relationship between {\sc lcf} and Isabelle. 
78 

79 Isabelle does not keep a record of inference steps. Each step is checked 

80 at run time to ensure that theorems can only be constructed by applying 

81 inference rules. An Isabelle proof typically involves hundreds of 

82 primitive inferences, and would be unintelligible if displayed. 

83 Discarding proofs saves vast amounts of storage. But can Isabelle be 

84 trusted? If desired, objectlogics can be formalized such that each 

85 theorem carries a proof term, which could be checked by another program. 

86 Proofs can also be traced. 

87 
78 
88 \index{Isabelle!release history} Isabelle was first distributed in 1986. 
79 \index{Isabelle!release history} Isabelle was first distributed in 1986. 
89 The 1987 version introduced a higherorder metalogic with an improved 
80 The 1987 version introduced a higherorder metalogic with an improved 
90 treatment of quantifiers. The 1988 version added limited polymorphism and 
81 treatment of quantifiers. The 1988 version added limited polymorphism and 
91 support for natural deduction. The 1989 version included a parser and 
82 support for natural deduction. The 1989 version included a parser and 
140 \include{foundations} 
131 \include{foundations} 
141 \include{getting} 
132 \include{getting} 
142 \include{advanced} 
133 \include{advanced} 
143 
134 
144 \bibliographystyle{plain} \small\raggedright\frenchspacing 
135 \bibliographystyle{plain} \small\raggedright\frenchspacing 
145 \bibliography{string,atp,funprog,general,logicprog,theory} 
136 \bibliography{string,atp,funprog,general,logicprog,isabelle,theory} 
146 
137 
147 \input{intro.ind} 
138 \input{intro.ind} 
148 \end{document} 
139 \end{document} 