Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
now mentions that the sections are available as
authorlcp
Thu, 15 Sep 1994 13:13:54 +0200
changeset 614 da97045ef59a
parent 613 f9eb0f819642
child 615 84ac5f101bd1
now mentions that the sections are available as Datatypes and (Co)Inductive Definitions in Isabelle/HOL
doc-src/ERRATA.txt file | annotate | diff | comparison | revisions 
--- 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)
isabelle