# HG changeset patch
# User nipkow
# Date 984587929 -3600
# Node ID 67cec35dbc58984388774751c0696ebf24bf9eb5
# Parent  bb01189f0565f5bc3da0092dae7a241b0b69dc46
*** empty log message ***

diff -r bb01189f0565 -r 67cec35dbc58 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Wed Mar 14 08:50:55 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Wed Mar 14 17:38:49 2001 +0100
@@ -17,12 +17,15 @@
 misled: HOL can express most mathematical concepts, and functional programming
 is just one particularly simple and ubiquitous instance.
 
-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.}
+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.
 
 A tutorial is by definition incomplete.  Currently the tutorial only
 introduces the rudiments of Isar's proof language. To fully exploit the power
diff -r bb01189f0565 -r 67cec35dbc58 doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Wed Mar 14 08:50:55 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Mar 14 17:38:49 2001 +0100
@@ -57,12 +57,6 @@
 
 Advanced recdef: explain recdef_tc?
 
-I guess we should say "HOL" everywhere, with a remark early on about the
-differences between our HOL and the other one.
-
-Syntax translations! Harpoons already used!
-say something about "abbreviations" when defs are introduced.
-
 warning: simp of asms from l to r; may require reordering (rotate_tac)
 
 Adjust FP textbook refs: new Bird, Hudak
diff -r bb01189f0565 -r 67cec35dbc58 doc-src/manual.bib
--- a/doc-src/manual.bib	Wed Mar 14 08:50:55 2001 +0100
+++ b/doc-src/manual.bib	Wed Mar 14 17:38:49 2001 +0100
@@ -91,8 +91,13 @@
 @InProceedings{Aspinall:TACAS:2000,
   author = 	 {David Aspinall},
   title = 	 {{P}roof {G}eneral: A Generic Tool for Proof Development},
-  booktitle = 	 {ETAPS / TACAS},
-  year =	 2000
+  booktitle = 	 {Tools and Algorithms for the Construction and Analysis of
+                  Systems (TACAS)},
+  year =	 2000,
+  publisher	= Springer,
+  series	= LNCS,
+  volume	= 1785,
+  pages = "38--42"
 }
 
 @Misc{isamode,
@@ -335,7 +340,7 @@
   note		= {Translated by Yves LaFont and Paul Taylor}}
 
 @Book{mgordon-hol,
-  author	= {M. J. C. Gordon and T. F. Melham},
+  editor	= {M. J. C. Gordon and T. F. Melham},
   title		= {Introduction to {HOL}: A Theorem Proving Environment for
 		 Higher Order Logic},
   publisher	= CUP,