ERRATA in Springer book
Thanks to Sara Kalvala, Tobias Nipkow
* = corrected by sending new pages
*page 50: In section heading, Mixfix should be mixfix
page 52: the declaration "types bool,nat" is illegal
*page 217 and 251: fst and snd should be fst_conv and snd_conv.
*Also affects index: pages 310 and 317!
pages 222, 223: The braces need escaping in
\tdx{qconverse_def} qconverse(r) == {z. w:r, EX x y. w= & z=}
\tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {}
\tdx{lfp_def} lfp(D,h) == Inter({X: Pow(D). h(X) <= X})
\tdx{gfp_def} gfp(D,h) == Union({X: Pow(D). X <= h(X)})
*page 224: type of id, namely $\To i$, should be $i \To i$
Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc]
should be addsimps
Ref/tactic: documented subgoals_tac
Ref/theories: added init_thy_reader and removed extend_theory.
Ref/defining: type constraints ("::") now have a very low priority of 4.
As in ML, they must be enclosed in paretheses most of the time.
Ref/syntax (page 145?): there is a repeated "the" in "before the the .thy file"
Logics/ZF: renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
renamed union_iff to Union_iff
renamed power_set to Pow_iff
DiffD2: now is really a destruction rule