diff -r f9eb0f819642 -r da97045ef59a doc-src/ERRATA.txt
--- 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)