1.1 --- a/doc-src/TutorialI/basics.tex	Wed Mar 14 08:50:55 2001 +0100
     1.2 +++ b/doc-src/TutorialI/basics.tex	Wed Mar 14 17:38:49 2001 +0100
     1.3 @@ -17,12 +17,15 @@
     1.4  misled: HOL can express most mathematical concepts, and functional programming
     1.5  is just one particularly simple and ubiquitous instance.
     1.6  
     1.7 -Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
     1.8 -This has influenced some of HOL's concrete syntax but is otherwise
     1.9 -irrelevant for us because this tutorial is based on
    1.10 -Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle
    1.11 -with structured proofs.\footnote{Thus the full name of the system should be
    1.12 -  Isabelle/Isar/HOL, but that is a bit of a mouthful.}
    1.13 +Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.  This has
    1.14 +influenced some of Isabelle/HOL's concrete syntax but is otherwise irrelevant
    1.15 +for us because this tutorial is based on
    1.16 +Isabelle/Isar~\cite{isabelle-isar-ref}, an extension of Isabelle with
    1.17 +structured proofs. Thus the full name of the system should be
    1.18 +Isabelle/Isar/HOL, but that is a bit of a mouthful. There are other
    1.19 +implementations of HOL, in particular the one by Mike Gordon \emph{et al.},
    1.20 +which is usually referred to as ``the HOL system'' \cite{mgordon-hol}. For us,
    1.21 +HOL refers to the logical system, and sometimes its incarnation Isabelle/HOL.
    1.22  
    1.23  A tutorial is by definition incomplete.  Currently the tutorial only
    1.24  introduces the rudiments of Isar's proof language. To fully exploit the power

     2.1 --- a/doc-src/TutorialI/todo.tobias	Wed Mar 14 08:50:55 2001 +0100
     2.2 +++ b/doc-src/TutorialI/todo.tobias	Wed Mar 14 17:38:49 2001 +0100
     2.3 @@ -57,12 +57,6 @@
     2.4  
     2.5  Advanced recdef: explain recdef_tc?
     2.6  
     2.7 -I guess we should say "HOL" everywhere, with a remark early on about the
     2.8 -differences between our HOL and the other one.
     2.9 -
    2.10 -Syntax translations! Harpoons already used!
    2.11 -say something about "abbreviations" when defs are introduced.
    2.12 -
    2.13  warning: simp of asms from l to r; may require reordering (rotate_tac)
    2.14  
    2.15  Adjust FP textbook refs: new Bird, Hudak

     3.1 --- a/doc-src/manual.bib	Wed Mar 14 08:50:55 2001 +0100
     3.2 +++ b/doc-src/manual.bib	Wed Mar 14 17:38:49 2001 +0100
     3.3 @@ -91,8 +91,13 @@
     3.4  @InProceedings{Aspinall:TACAS:2000,
     3.5    author = 	 {David Aspinall},
     3.6    title = 	 {{P}roof {G}eneral: A Generic Tool for Proof Development},
     3.7 -  booktitle = 	 {ETAPS / TACAS},
     3.8 -  year =	 2000
     3.9 +  booktitle = 	 {Tools and Algorithms for the Construction and Analysis of
    3.10 +                  Systems (TACAS)},
    3.11 +  year =	 2000,
    3.12 +  publisher	= Springer,
    3.13 +  series	= LNCS,
    3.14 +  volume	= 1785,
    3.15 +  pages = "38--42"
    3.16  }
    3.17  
    3.18  @Misc{isamode,
    3.19 @@ -335,7 +340,7 @@
    3.20    note		= {Translated by Yves LaFont and Paul Taylor}}
    3.21  
    3.22  @Book{mgordon-hol,
    3.23 -  author	= {M. J. C. Gordon and T. F. Melham},
    3.24 +  editor	= {M. J. C. Gordon and T. F. Melham},
    3.25    title		= {Introduction to {HOL}: A Theorem Proving Environment for
    3.26  		 Higher Order Logic},
    3.27    publisher	= CUP,