Added primrec section
authornipkow
Sun, 11 Sep 1994 12:52:00 +0200
changeset 601208834a9ba70
parent 600 d9133e7ed38a
child 602 9cb1fa628dbb
Added primrec section
doc-src/ERRATA.txt
     1.1 --- a/doc-src/ERRATA.txt	Sun Sep 11 10:59:09 1994 +0200
     1.2 +++ b/doc-src/ERRATA.txt	Sun Sep 11 12:52:00 1994 +0200
     1.3 @@ -81,8 +81,9 @@
     1.4  	PowI     A<=B ==> A: Pow(B)
     1.5  	PowD     A: Pow(B) ==> A<=B
     1.6  
     1.7 -page 259: HOL theory files may now include datatype declarations and
     1.8 -(co)inductive definitions.  (Two sections added.)
     1.9 +page 259: HOL theory files may now include datatype declarations, primitive
    1.10 +recursive function definitions, and (co)inductive definitions.  (Three
    1.11 +sections added.)
    1.12  
    1.13  page 259: now there is another examples directory, IMP (a semantics
    1.14  equivalence proof for an imperative language)