# HG changeset patch
# User nipkow
# Date 985001916 -3600
# Node ID aeb5c72dd72a213775c63c1cd9836283ade7771f
# Parent  d06fb91f22daceaae11ba5b4ac980621f2ffd9d5
*** empty log message ***

diff -r d06fb91f22da -r aeb5c72dd72a doc-src/TutorialI/Types/Overloading0.thy
--- 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
diff -r d06fb91f22da -r aeb5c72dd72a doc-src/TutorialI/Types/document/Overloading0.tex
--- 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
diff -r d06fb91f22da -r aeb5c72dd72a doc-src/TutorialI/Types/types.tex
--- 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
diff -r d06fb91f22da -r aeb5c72dd72a doc-src/TutorialI/basics.tex
--- 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
diff -r d06fb91f22da -r aeb5c72dd72a doc-src/TutorialI/fp.tex
--- 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
diff -r d06fb91f22da -r aeb5c72dd72a doc-src/TutorialI/tutorial.tex
--- 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