8 HOL, which abbreviates HigherOrder Logic. We introduce HOL step by step 
8 HOL, which abbreviates HigherOrder Logic. We introduce HOL step by step 
9 following the equation 
9 following the equation 
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] 
10 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] 
11 We assume that the reader is familiar with the basic concepts of both fields. 
11 We assume that the reader is familiar with the basic concepts of both fields. 
12 For excellent introductions to functional programming consult the textbooks 
12 For excellent introductions to functional programming consult the textbooks 
13 by Bird and Wadler~\cite{BirdWadler} or Paulson~\cite{PaulsonML}. Although 
13 by Bird and Wadler~\cite{BirdWadler} or Paulson~\cite{paulsonml2}. Although 
14 this tutorial initially concentrates on functional programming, do not be 
14 this tutorial initially concentrates on functional programming, do not be 
15 misled: HOL can express most mathematical concepts, and functional 
15 misled: HOL can express most mathematical concepts, and functional 
16 programming is just one particularly simple and ubiquitous instance. 
16 programming is just one particularly simple and ubiquitous instance. 
17 
17 
18 A tutorial is by definition incomplete. To fully exploit the power of the 
18 A tutorial is by definition incomplete. To fully exploit the power of the 
19 system you need to consult the Isabelle Reference Manual~\cite{IsaRefMan} 
19 system you need to consult the Isabelle Reference Manual~\cite{isabelleref} 
20 for details about Isabelle and the HOL chapter of the Logics 
20 for details about Isabelle and the Isabelle/HOL manual~\cite{isabelleHOL} 
21 manual~\cite{IsaLogicsMan} for details relating to HOL. Both manuals have a 
21 for details relating to HOL. Both manuals have a comprehensive index. 
22 comprehensive index. 

23 
22 
24 \section{Theories, proofs and interaction} 
23 \section{Theories, proofs and interaction} 
25 \label{sec:Basic:Theories} 
24 \label{sec:Basic:Theories} 
26 
25 
27 Working with Isabelle means creating two different kinds of documents: 
26 Working with Isabelle means creating two different kinds of documents: 
56 \end{warn} 
55 \end{warn} 
57 
56 
58 This tutorial is concerned with introducing you to the different linguistic 
57 This tutorial is concerned with introducing you to the different linguistic 
59 constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template. 
58 constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template. 
60 A complete grammar of the basic constructs is found in Appendix~A 
59 A complete grammar of the basic constructs is found in Appendix~A 
61 of~\cite{IsaRefMan}, for reference in times of doubt. 
60 of~\cite{isabelleref}, for reference in times of doubt. 
62 
61 
63 The tutorial is also concerned with showing you how to prove theorems about 
62 The tutorial is also concerned with showing you how to prove theorems about 
64 the concepts in a theory. This involves invoking predefined theorem proving 
63 the concepts in a theory. This involves invoking predefined theorem proving 
65 commands. Because Isabelle is written in the programming language 
64 commands. Because Isabelle is written in the programming language 
66 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not 
65 ML,\footnote{Many concepts in HOL and ML are similar. Make sure you do not 