--- a/doc-src/ERRATA.txt Wed Sep 14 16:11:19 1994 +0200
+++ b/doc-src/ERRATA.txt Thu Sep 15 13:13:54 1994 +0200
@@ -82,8 +82,9 @@
PowD A: Pow(B) ==> A<=B
page 259: HOL theory files may now include datatype declarations, primitive
-recursive function definitions, and (co)inductive definitions. (Three
-sections added.)
+recursive function definitions, and (co)inductive definitions. (These new
+sections are available separately as the file ml/HOL-extensions.dvi.gz,
+host ftp.cl.cam.ac.uk.)
page 259: now there is another examples directory, IMP (a semantics
equivalence proof for an imperative language)