--- a/doc-src/TutorialI/Types/Overloading0.thy Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/Types/Overloading0.thy Mon Mar 19 12:38:36 2001 +0100
@@ -33,7 +33,7 @@
warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
-@{text"inverse []"} and proving theorems as @{text"inverse []
+@{text"inverse []"} and proving theorems such as @{text"inverse []
= inverse []"}, although we never defined inverse on lists. We hasten to say
that there is nothing wrong with such terms and theorems. But it would be
nice if we could prevent their formation, simply because it is very likely
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Mon Mar 19 12:38:36 2001 +0100
@@ -37,7 +37,7 @@
warnings to that effect.
However, there is nothing to prevent the user from forming terms such as
-\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, although we never defined inverse on lists. We hasten to say
+\isa{inverse\ {\isacharbrackleft}{\isacharbrackright}} and proving theorems such as \isa{inverse\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ inverse\ {\isacharbrackleft}{\isacharbrackright}}, although we never defined inverse on lists. We hasten to say
that there is nothing wrong with such terms and theorems. But it would be
nice if we could prevent their formation, simply because it is very likely
that the user did not mean to write what he did. Thus she had better not waste
--- a/doc-src/TutorialI/Types/types.tex Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/Types/types.tex Mon Mar 19 12:38:36 2001 +0100
@@ -43,7 +43,7 @@
Isabelle offers the related concept of an \textbf{axiomatic type class}.
Roughly speaking, an axiomatic type class is a type class with axioms, i.e.\
an axiomatic specification of a class of types. Thus we can talk about a type
-$t$ being in a class $C$, which is written $\tau :: C$. This is the case if
+$\tau$ being in a class $C$, which is written $\tau :: C$. This is the case if
$\tau$ satisfies the axioms of $C$. Furthermore, type classes can be
organized in a hierarchy. Thus there is the notion of a class $D$ being a
\textbf{subclass} of a class $C$, written $D < C$. This is the case if all
--- a/doc-src/TutorialI/basics.tex Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/basics.tex Mon Mar 19 12:38:36 2001 +0100
@@ -20,16 +20,19 @@
Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}. This has
influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
for us because this tutorial is based on
-Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with
-structured proofs. Thus the full name of the system should be
-Isabelle/Isar/HOL, but that is a bit of a mouthful. There are other
-implementations of HOL, in particular the one by Mike Gordon \emph{et al.},
-which is usually referred to as ``the HOL system'' \cite{mgordon-hol}. For us,
-HOL refers to the logical system, and sometimes its incarnation Isabelle/HOL.
+Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle which hides
+the implementation language almost completely. Thus the full name of the
+system should be Isabelle/Isar/HOL, but that is a bit of a mouthful.
+
+There are other implementations of HOL, in particular the one by Mike Gordon
+\emph{et al.}, which is usually referred to as ``the HOL system''
+\cite{mgordon-hol}. For us, HOL refers to the logical system, and sometimes
+its incarnation Isabelle/HOL.
A tutorial is by definition incomplete. Currently the tutorial only
introduces the rudiments of Isar's proof language. To fully exploit the power
-of Isar you need to consult the Isabelle/Isar Reference
+of Isar, in particular the ability to write readable and structured proofs,
+you need to consult the Isabelle/Isar Reference
Manual~\cite{isabelle-isar-ref}. If you want to use Isabelle's ML level
directly (for example for writing your own proof procedures) see the Isabelle
Reference Manual~\cite{isabelle-ref}; for details relating to HOL see the
--- a/doc-src/TutorialI/fp.tex Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Mon Mar 19 12:38:36 2001 +0100
@@ -284,7 +284,7 @@
(except real axioms) is reduced to a definition. For example, given some
\isacommand{primrec} function definition, this is turned into a proper
(nonrecursive!) definition, and the user-supplied recursion equations are
-derived as theorems from the definition. This tricky process is completely
+derived as theorems from that definition. This tricky process is completely
hidden from the user and it is not necessary to understand the details. The
result of the definitional approach is that \isacommand{primrec} is as safe
as pure \isacommand{defs} are, but more convenient. And this is not just the
--- a/doc-src/TutorialI/tutorial.tex Mon Mar 19 10:37:47 2001 +0100
+++ b/doc-src/TutorialI/tutorial.tex Mon Mar 19 12:38:36 2001 +0100
@@ -77,8 +77,8 @@
\subsubsection*{Acknowledgements}
This tutorial owes a lot to the constant discussions with and the valuable
feedback from the Isabelle group at Munich: Stefan Berghofer, Olaf M{\"u}ller,
-Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
-and Markus Wenzel. Stephan Merz was also kind enough to
+Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch,
+Martin Strecker and Markus Wenzel. Stephan Merz was also kind enough to
read and comment on a draft version.
\clearfirst