|
456
|
1 |
ERRATA in Springer book
|
|
|
2 |
|
|
491
|
3 |
Thanks to Sara Kalvala, Tobias Nipkow
|
|
|
4 |
|
|
456
|
5 |
* = corrected by sending new pages
|
|
|
6 |
|
|
|
7 |
*page 50: In section heading, Mixfix should be mixfix
|
|
|
8 |
|
|
|
9 |
*page 217 and 251: fst and snd should be fst_conv and snd_conv.
|
|
|
10 |
*Also affects index: pages 310 and 317!
|
|
|
11 |
|
|
|
12 |
*page 224: type of id, namely $\To i$, should be $i \To i$
|
|
|
13 |
|
|
507
|
14 |
Intro/advanced
|
|
|
15 |
page 52: the declaration "types bool,nat" is illegal
|
|
|
16 |
|
|
|
17 |
should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]'
|
|
|
18 |
|
|
|
19 |
|
|
|
20 |
Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing}
|
|
|
21 |
|
|
|
22 |
Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control}
|
|
456
|
23 |
|
|
|
24 |
Ref/tactic: documented subgoals_tac
|
|
|
25 |
|
|
491
|
26 |
Ref/theories: added init_thy_reader and removed extend_theory.
|
|
458
|
27 |
|
|
|
28 |
Ref/defining: type constraints ("::") now have a very low priority of 4.
|
|
|
29 |
As in ML, they must be enclosed in paretheses most of the time.
|
|
479
|
30 |
|
|
507
|
31 |
Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file"
|
|
491
|
32 |
|
|
507
|
33 |
Logics/ZF: ****************
|
|
|
34 |
renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl
|
|
491
|
35 |
renamed union_iff to Union_iff
|
|
|
36 |
renamed power_set to Pow_iff
|
|
|
37 |
DiffD2: now is really a destruction rule
|
|
507
|
38 |
escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def
|
|
|
39 |
|