diff -r c2754409919b -r 94b638b3827c doc-src/Tutorial/basics.tex --- a/doc-src/Tutorial/basics.tex Thu May 06 11:13:01 1999 +0200 +++ b/doc-src/Tutorial/basics.tex Thu May 06 11:48:09 1999 +0200 @@ -10,16 +10,15 @@ $\mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}.$ We assume that the reader is familiar with the basic concepts of both fields. For excellent introductions to functional programming consult the textbooks -by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{Paulson-ML}. Although +by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}. Although this tutorial initially concentrates on functional programming, do not be misled: HOL can express most mathematical concepts, and functional programming is just one particularly simple and ubiquitous instance. A tutorial is by definition incomplete. To fully exploit the power of the -system you need to consult the Isabelle Reference Manual~\cite{Isa-Ref-Man} -for details about Isabelle and the HOL chapter of the Logics -manual~\cite{Isa-Logics-Man} for details relating to HOL. Both manuals have a -comprehensive index. +system you need to consult the Isabelle Reference Manual~\cite{isabelle-ref} +for details about Isabelle and the Isabelle/HOL manual~\cite{isabelle-HOL} +for details relating to HOL. Both manuals have a comprehensive index. \section{Theories, proofs and interaction} \label{sec:Basic:Theories} @@ -58,7 +57,7 @@ This tutorial is concerned with introducing you to the different linguistic constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template. A complete grammar of the basic constructs is found in Appendix~A -of~\cite{Isa-Ref-Man}, for reference in times of doubt. +of~\cite{isabelle-ref}, for reference in times of doubt. The tutorial is also concerned with showing you how to prove theorems about the concepts in a theory. This involves invoking predefined theorem proving