--- a/doc-src/ERRATA.txt Sun Sep 11 10:59:09 1994 +0200
+++ b/doc-src/ERRATA.txt Sun Sep 11 12:52:00 1994 +0200
@@ -81,8 +81,9 @@
PowI A<=B ==> A: Pow(B)
PowD A: Pow(B) ==> A<=B
-page 259: HOL theory files may now include datatype declarations and
-(co)inductive definitions. (Two sections added.)
+page 259: HOL theory files may now include datatype declarations, primitive
+recursive function definitions, and (co)inductive definitions. (Three
+sections added.)
page 259: now there is another examples directory, IMP (a semantics
equivalence proof for an imperative language)