1.1 --- a/doc-src/ERRATA.txt	Wed Aug 03 09:45:42 1994 +0200
     1.2 +++ b/doc-src/ERRATA.txt	Thu Aug 04 11:45:59 1994 +0200
     1.3 @@ -6,21 +6,20 @@
     1.4  
     1.5  *page 50: In section heading, Mixfix should be mixfix
     1.6  
     1.7 -page 52: the declaration  "types bool,nat"  is illegal    
     1.8 -
     1.9  *page 217 and 251: fst and snd should be fst_conv and snd_conv.
    1.10  *Also affects index: pages 310 and 317!
    1.11  
    1.12 -pages 222, 223: The braces need escaping in
    1.13 -\tdx{qconverse_def}   qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>}
    1.14 -\tdx{QSigma_def}      QSigma(A,B)  == UN x:A. UN y:B(x). {<x;y>}
    1.15 -\tdx{lfp_def}        lfp(D,h) == Inter({X: Pow(D). h(X) <= X})
    1.16 -\tdx{gfp_def}        gfp(D,h) == Union({X: Pow(D). X <= h(X)})
    1.17 -
    1.18  *page 224: type of id, namely $\To i$, should be $i \To i$ 
    1.19  
    1.20 -Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc]
    1.21 -should be addsimps
    1.22 +Intro/advanced
    1.23 +page 52: the declaration  "types bool,nat"  is illegal    
    1.24 +
    1.25 +should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]'
    1.26 +
    1.27 +
    1.28 +Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing}
    1.29 +
    1.30 +Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control}
    1.31  
    1.32  Ref/tactic: documented subgoals_tac
    1.33  
    1.34 @@ -29,9 +28,12 @@
    1.35  Ref/defining: type constraints ("::") now have a very low priority of 4.
    1.36                As in ML, they must be enclosed in paretheses most of the time.
    1.37  
    1.38 -Ref/syntax (page 145?): there is a repeated "the" in "before the the .thy file"
    1.39 +Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file"
    1.40  
    1.41 -Logics/ZF: renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
    1.42 +Logics/ZF: ****************
    1.43 +renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
    1.44  renamed union_iff to Union_iff
    1.45  renamed power_set to Pow_iff
    1.46  DiffD2: now is really a destruction rule
    1.47 +escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def
    1.48 +