doc-src/ERRATA.txt
changeset 601 208834a9ba70
parent 599 08b403fe92b1
child 614 da97045ef59a
equal deleted inserted replaced
600:d9133e7ed38a 601:208834a9ba70
    79 
    79 
    80 page 248: Pow has the rules
    80 page 248: Pow has the rules
    81 	PowI     A<=B ==> A: Pow(B)
    81 	PowI     A<=B ==> A: Pow(B)
    82 	PowD     A: Pow(B) ==> A<=B
    82 	PowD     A: Pow(B) ==> A<=B
    83 
    83 
    84 page 259: HOL theory files may now include datatype declarations and
    84 page 259: HOL theory files may now include datatype declarations, primitive
    85 (co)inductive definitions.  (Two sections added.)
    85 recursive function definitions, and (co)inductive definitions.  (Three
       
    86 sections added.)
    86 
    87 
    87 page 259: now there is another examples directory, IMP (a semantics
    88 page 259: now there is another examples directory, IMP (a semantics
    88 equivalence proof for an imperative language)
    89 equivalence proof for an imperative language)