doc-src/ERRATA.txt
changeset 491 1a7717eca145
parent 479 db5a95f2952e
child 507 a00301e9e64b
     1.1 --- a/doc-src/ERRATA.txt	Wed Jul 27 16:09:14 1994 +0200
     1.2 +++ b/doc-src/ERRATA.txt	Wed Jul 27 19:04:21 1994 +0200
     1.3 @@ -1,5 +1,7 @@
     1.4  ERRATA in Springer book
     1.5  
     1.6 +Thanks to Sara Kalvala, Tobias Nipkow
     1.7 +
     1.8  * = corrected by sending new pages
     1.9  
    1.10  *page 50: In section heading, Mixfix should be mixfix
    1.11 @@ -22,9 +24,14 @@
    1.12  
    1.13  Ref/tactic: documented subgoals_tac
    1.14  
    1.15 -Logics/ZF: renamed mem_anti_sym and mem_anti_refl
    1.16 +Ref/theories: added init_thy_reader and removed extend_theory.
    1.17  
    1.18  Ref/defining: type constraints ("::") now have a very low priority of 4.
    1.19                As in ML, they must be enclosed in paretheses most of the time.
    1.20  
    1.21 -Ref/theories: added init_thy_reader and removed extend_theory.
    1.22 +Ref/syntax (page 145?): there is a repeated "the" in "before the the .thy file"
    1.23 +
    1.24 +Logics/ZF: renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
    1.25 +renamed union_iff to Union_iff
    1.26 +renamed power_set to Pow_iff
    1.27 +DiffD2: now is really a destruction rule