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