summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/ERRATA.txt

changeset 701 | 74ee8b9ff9a7 |

parent 614 | da97045ef59a |

child 716 | 79adbdbda0fb |

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,