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