summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Tutorial/basics.tex

changeset 6606 | 94b638b3827c |

parent 6584 | 5569f2672662 |

child 6628 | 12ed4f748f7c |

--- 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