1.1 --- a/doc-src/ERRATA.txt	Mon Nov 21 10:39:32 1994 +0100
     1.2 +++ b/doc-src/ERRATA.txt	Mon Nov 21 10:51:40 1994 +0100
     1.3 @@ -38,6 +38,8 @@
     1.4  
     1.5  Defining Logics
     1.6  
     1.7 +
     1.8 +
     1.9  page 127: type constraints ("::") now have a very low priority of 4.
    1.10  As in ML, they must usually be enclosed in paretheses.
    1.11  
    1.12 @@ -47,13 +49,22 @@
    1.13  
    1.14  Simplification
    1.15  
    1.16 +page 157 display: Union operator is too big
    1.17 +
    1.18  page 158, "!": Isabelle now permits more general left-hand sides, so called
    1.19  higher-order patterns.
    1.20  
    1.21 +
    1.22  ISABELLE'S OBJECT-LOGICS
    1.23  
    1.24 +First-Order Logic
    1.25 +
    1.26 +page 191: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead)
    1.27 +
    1.28  Zermelo-Fraenkel Set Theory
    1.29  
    1.30 +page 204: type i has class term, not (just) logic
    1.31 +
    1.32  page 209: axioms have been renamed:
    1.33  	union_iff is now Union_iff
    1.34  	power_set is now Pow_iff
    1.35 @@ -91,6 +102,8 @@
    1.36  page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c
    1.37  Definition and rules modified accordingly
    1.38  
    1.39 +page 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead)
    1.40 +
    1.41  page 254: nat_case now has type ['a, nat=>'a, nat] =>'a
    1.42  Definition modified accordingly
    1.43