1.1 --- a/doc-src/ERRATA.txt	Thu Nov 10 11:36:40 1994 +0100
     1.2 +++ b/doc-src/ERRATA.txt	Fri Nov 11 10:31:51 1994 +0100
     1.3 @@ -81,6 +81,18 @@
     1.4  	PowI     A<=B ==> A: Pow(B)
     1.5  	PowD     A: Pow(B) ==> A<=B
     1.6  
     1.7 +page 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'c
     1.8 +Definition modified accordingly
     1.9 +
    1.10 +page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c
    1.11 +Definition and rules modified accordingly
    1.12 +
    1.13 +page 254: nat_case now has type ['a, nat=>'a, nat] =>'a
    1.14 +Definition modified accordingly
    1.15 +
    1.16 +page 256,258: list_case now takes the list as its last argument, not the
    1.17 +first.
    1.18 +
    1.19  page 259: HOL theory files may now include datatype declarations, primitive
    1.20  recursive function definitions, and (co)inductive definitions.  (These new
    1.21  sections are available separately as the file ml/HOL-extensions.dvi.gz,