--- 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
--- 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
--- 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,