summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/ERRATA.txt

changeset 718 | efca1e0710fb |

parent 716 | 79adbdbda0fb |

child 863 | 67692db44c70 |

--- a/doc-src/ERRATA.txt Mon Nov 21 10:39:32 1994 +0100 +++ b/doc-src/ERRATA.txt Mon Nov 21 10:51:40 1994 +0100 @@ -38,6 +38,8 @@ Defining Logics + + page 127: type constraints ("::") now have a very low priority of 4. As in ML, they must usually be enclosed in paretheses. @@ -47,13 +49,22 @@ Simplification +page 157 display: Union operator is too big + page 158, "!": Isabelle now permits more general left-hand sides, so called higher-order patterns. + ISABELLE'S OBJECT-LOGICS +First-Order Logic + +page 191: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead) + Zermelo-Fraenkel Set Theory +page 204: type i has class term, not (just) logic + page 209: axioms have been renamed: union_iff is now Union_iff power_set is now Pow_iff @@ -91,6 +102,8 @@ page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c Definition and rules modified accordingly +page 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead) + page 254: nat_case now has type ['a, nat=>'a, nat] =>'a Definition modified accordingly