author nipkow Thu, 06 May 1999 11:48:09 +0200 changeset 6606 94b638b3827c parent 6605 c2754409919b child 6607 df9b0abf77e0
Refs.
 doc-src/Tutorial/basics.tex file | annotate | diff | comparison | revisions doc-src/Tutorial/fp.tex file | annotate | diff | comparison | revisions
--- 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
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
--- a/doc-src/Tutorial/fp.tex	Thu May 06 11:13:01 1999 +0200
+++ b/doc-src/Tutorial/fp.tex	Thu May 06 11:48:09 1999 +0200
@@ -382,7 +382,7 @@
constructor names and $\tau@{ij}$ are types; it is customary to capitalize
the first letter in constructor names. There are a number of
restrictions (such as the type should not be empty) detailed
-elsewhere~\cite{Isa-Logics-Man}. Isabelle notifies you if you violate them.
+elsewhere~\cite{isabelle-HOL}. Isabelle notifies you if you violate them.

Laws about datatypes, such as \verb$[] ~= x#xs$ and \texttt{(x\#xs = y\#ys) =
(x=y \& xs=ys)}, are used automatically during proofs by simplification.
@@ -1068,7 +1068,7 @@
is commutativity: $x+y = y+x$.  Another example is $(x-y)-z = (x-z)-y$.  Such
rules are problematic because once they apply, they can be used forever.
The simplifier is aware of this danger and treats permutative rules
-separately. For details see~\cite{Isa-Ref-Man}.
+separately. For details see~\cite{isabelle-ref}.

\subsubsection{Tracing}
\indexbold{tracing the simplifier}
@@ -1486,13 +1486,13 @@

For a theoretical analysis of what kinds of datatypes are feasible in HOL
see, for example,~\cite{Gunter-HOL92}. There are alternatives to pure HOL:
-LCF~\cite{Paulson-LCF} is a logic where types like
+LCF~\cite{paulson87} is a logic where types like
\begin{ttbox}
datatype t = C (t -> t)
\end{ttbox}
do indeed make sense (note the intentionally different arrow \texttt{->}!).
There is even a version of LCF on top of HOL, called
-HOLCF~\cite{MuellerNvOS98}.
+HOLCF~\cite{MuellerNvOS99}.

\index{*primrec|)}
\index{*datatype|)}
@@ -1737,7 +1737,7 @@
Ackermann's function requires the lexicographic product \texttt{**}:
\begin{ttbox}
\input{Recdef/ack}\end{ttbox}
-For details see the manual~\cite{Isa-Logics-Man} and the examples in the
+For details see the manual~\cite{isabelle-HOL} and the examples in the
library.