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 251: split now has type [['a,'b] => 'c, 'a * 'b] => 'c 

85 Definition modified accordingly 

86 

87 page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c 

88 Definition and rules modified accordingly 

89 

90 page 254: nat_case now has type ['a, nat=>'a, nat] =>'a 

91 Definition modified accordingly 

92 

93 page 256,258: list_case now takes the list as its last argument, not the 

94 first. 

95 
84 page 259: HOL theory files may now include datatype declarations, primitive 
96 page 259: HOL theory files may now include datatype declarations, primitive 
85 recursive function definitions, and (co)inductive definitions. (These new 
97 recursive function definitions, and (co)inductive definitions. (These new 
86 sections are available separately as the file ml/HOLextensions.dvi.gz, 
98 sections are available separately as the file ml/HOLextensions.dvi.gz, 
87 host ftp.cl.cam.ac.uk.) 
99 host ftp.cl.cam.ac.uk.) 
88 
100 