equal
deleted
inserted
replaced
1 ERRATA in Springer book |
1 ERRATA in Springer book |
|
2 |
|
3 Thanks to Sara Kalvala, Tobias Nipkow |
2 |
4 |
3 * = corrected by sending new pages |
5 * = corrected by sending new pages |
4 |
6 |
5 *page 50: In section heading, Mixfix should be mixfix |
7 *page 50: In section heading, Mixfix should be mixfix |
6 |
8 |
20 Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc] |
22 Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc] |
21 should be addsimps |
23 should be addsimps |
22 |
24 |
23 Ref/tactic: documented subgoals_tac |
25 Ref/tactic: documented subgoals_tac |
24 |
26 |
25 Logics/ZF: renamed mem_anti_sym and mem_anti_refl |
27 Ref/theories: added init_thy_reader and removed extend_theory. |
26 |
28 |
27 Ref/defining: type constraints ("::") now have a very low priority of 4. |
29 Ref/defining: type constraints ("::") now have a very low priority of 4. |
28 As in ML, they must be enclosed in paretheses most of the time. |
30 As in ML, they must be enclosed in paretheses most of the time. |
29 |
31 |
30 Ref/theories: added init_thy_reader and removed extend_theory. |
32 Ref/syntax (page 145?): there is a repeated "the" in "before the the .thy file" |
|
33 |
|
34 Logics/ZF: renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl |
|
35 renamed union_iff to Union_iff |
|
36 renamed power_set to Pow_iff |
|
37 DiffD2: now is really a destruction rule |