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/HOL-extensions.dvi.gz, |
98 sections are available separately as the file ml/HOL-extensions.dvi.gz, |
87 host ftp.cl.cam.ac.uk.) |
99 host ftp.cl.cam.ac.uk.) |
88 |
100 |