summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Fri, 11 Nov 1994 10:31:51 +0100 | |

changeset 701 | 74ee8b9ff9a7 |

parent 700 | 31f50c1778ef |

child 702 | 98fc1a8e832a |

argument swaps in HOL

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