diff -r 7917e66505a4 -r 6852682eaf16 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Wed Jan 24 11:59:15 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Wed Jan 24 12:29:10 2001 +0100
@@ -2,7 +2,7 @@
 
 \section{Introduction}
 
-This is a tutorial on how to use Isabelle/HOL as a specification and
+This is a tutorial on how to use the theorem prover Isabelle/HOL as a specification and
 verification system. Isabelle is a generic system for implementing logical
 formalisms, and Isabelle/HOL is the specialization of Isabelle for
 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
@@ -15,13 +15,12 @@
 misled: HOL can express most mathematical concepts, and functional
 programming is just one particularly simple and ubiquitous instance.
 
-This tutorial introduces HOL via Isabelle/Isar~\cite{isabelle-isar-ref},
-which is an extension of Isabelle~\cite{paulson-isa-book} with structured
-proofs.\footnote{Thus the full name of the system should be
-  Isabelle/Isar/HOL, but that is a bit of a mouthful.} The most noticeable
-difference to classical Isabelle (which is the basis of another version of
-this tutorial) is the replacement of the ML level by a dedicated language for
-definitions and proofs.
+Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
+This has influenced some of 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.\footnote{Thus the full name of the system should be
+  Isabelle/Isar/HOL, but that is a bit of a mouthful.}
 
 A tutorial is by definition incomplete.  Currently the tutorial only
 introduces the rudiments of Isar's proof language. To fully exploit the power
@@ -74,7 +73,7 @@
   HOL contains a theory \isaindexbold{Main}, the union of all the basic
   predefined theories like arithmetic, lists, sets, etc.  
   Unless you know what you are doing, always include \isa{Main}
-  as a direct or indirect parent theory of all your theories.
+  as a direct or indirect parent of all your theories.
 \end{warn}
 
 
@@ -122,7 +121,8 @@
 \end{ttbox}
 
 \noindent
-This can be reversed by \texttt{ML "reset show_types"}. Various other flags
+This can be reversed by \texttt{ML "reset show_types"}. Various other flags,
+which we introduce as we go along,
 can be set and reset in the same manner.\indexbold{flag!(re)setting}
 \end{warn}
 
@@ -196,7 +196,7 @@
 should be familiar with to avoid certain syntactic traps. A particular
 problem for novices can be the priority of operators. If you are unsure, use
 additional parentheses. In those cases where Isabelle echoes your
-input, you can see which parentheses are dropped---they were superfluous. If
+input, you can see which parentheses are dropped --- they were superfluous. If
 you are unsure how to interpret Isabelle's output because you don't know
 where the (dropped) parentheses go, set the \rmindex{flag}
 \isaindexbold{show_brackets}:
@@ -222,7 +222,7 @@
 \item
 Constructs with an opening but without a closing delimiter bind very weakly
 and should therefore be enclosed in parentheses if they appear in subterms, as
-in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
+in \isa{(\isasymlambda{}x.~x) = f}. This includes \isaindex{if},
 \isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
 \item
 Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}