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)