4 |
4 |
5 * = corrected by sending new pages |
5 * = corrected by sending new pages |
6 |
6 |
7 *page 50: In section heading, Mixfix should be mixfix |
7 *page 50: In section heading, Mixfix should be mixfix |
8 |
8 |
9 page 52: the declaration "types bool,nat" is illegal |
|
10 |
|
11 *page 217 and 251: fst and snd should be fst_conv and snd_conv. |
9 *page 217 and 251: fst and snd should be fst_conv and snd_conv. |
12 *Also affects index: pages 310 and 317! |
10 *Also affects index: pages 310 and 317! |
13 |
11 |
14 pages 222, 223: The braces need escaping in |
|
15 \tdx{qconverse_def} qconverse(r) == {z. w:r, EX x y. w=<x;y> & z=<y;x>} |
|
16 \tdx{QSigma_def} QSigma(A,B) == UN x:A. UN y:B(x). {<x;y>} |
|
17 \tdx{lfp_def} lfp(D,h) == Inter({X: Pow(D). h(X) <= X}) |
|
18 \tdx{gfp_def} gfp(D,h) == Union({X: Pow(D). X <= h(X)}) |
|
19 |
|
20 *page 224: type of id, namely $\To i$, should be $i \To i$ |
12 *page 224: type of id, namely $\To i$, should be $i \To i$ |
21 |
13 |
22 Intro/advanced.tex:val add_ss = FOL_ss addrews [add_0, add_Suc] |
14 Intro/advanced |
23 should be addsimps |
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} |
24 |
23 |
25 Ref/tactic: documented subgoals_tac |
24 Ref/tactic: documented subgoals_tac |
26 |
25 |
27 Ref/theories: added init_thy_reader and removed extend_theory. |
26 Ref/theories: added init_thy_reader and removed extend_theory. |
28 |
27 |
29 Ref/defining: type constraints ("::") now have a very low priority of 4. |
28 Ref/defining: type constraints ("::") now have a very low priority of 4. |
30 As in ML, they must be enclosed in paretheses most of the time. |
29 As in ML, they must be enclosed in paretheses most of the time. |
31 |
30 |
32 Ref/syntax (page 145?): there is a repeated "the" in "before the the .thy file" |
31 Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file" |
33 |
32 |
34 Logics/ZF: renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl |
33 Logics/ZF: **************** |
|
34 renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl |
35 renamed union_iff to Union_iff |
35 renamed union_iff to Union_iff |
36 renamed power_set to Pow_iff |
36 renamed power_set to Pow_iff |
37 DiffD2: now is really a destruction rule |
37 DiffD2: now is really a destruction rule |
|
38 escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def |
|
39 |