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