# HG changeset patch
# User lcp
# Date 779627634 -7200
# Node ID da97045ef59a380dcb7981c9bd945f6f3068e0e1
# Parent  f9eb0f819642b2ad77119dbf8935bf13248f205d
now mentions that the sections are available as
Datatypes and (Co)Inductive Definitions in Isabelle/HOL

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)