1 ERRATA in Springer book |
1 $Id$ |
|
2 ERRATA in the book "Isabelle: A Generic Theorem Prover" |
|
3 by Lawrence C. Paulson (contributions by Tobias Nipkow) |
|
4 |
|
5 Some of these errors are typographical but most of them are due to continuing |
|
6 changes to Isabelle. |
2 |
7 |
3 Thanks to Sara Kalvala, Tobias Nipkow |
8 Thanks to Sara Kalvala, Tobias Nipkow |
4 |
9 |
5 * = corrected by sending new pages |
|
6 |
10 |
7 *page 50: In section heading, Mixfix should be mixfix |
11 INTRODUCTION TO ISABELLE |
8 |
12 |
9 *page 217 and 251: fst and snd should be fst_conv and snd_conv. |
13 Advanced Methods |
10 *Also affects index: pages 310 and 317! |
|
11 |
14 |
12 *page 224: type of id, namely $\To i$, should be $i \To i$ |
15 page 52, middle: the declaration "types bool,nat" should be "types bool nat" |
13 |
16 |
14 Intro/advanced |
17 page 57, bottom: should be addsimps in |
15 page 52: the declaration "types bool,nat" is illegal |
18 val add_ss = FOL_ss addrews [add_0, add_Suc] |
16 |
|
17 should be addsimps in 'val add_ss = FOL_ss addrews [add_0, add_Suc]' |
|
18 |
19 |
19 |
20 |
20 Ref/introduction: documented show_brackets; added\pageref{sec:goals-printing} |
21 ISABELLE REFERENCE MANUAL |
21 |
22 |
22 Ref/goals: in 'Printing the proof state' added \ref{sec:printing-control} |
23 Introduction |
23 |
24 |
24 Ref/tactic: documented subgoals_tac |
25 page 67: show_brackets is another flag, controlling display of bracketting |
25 |
26 |
26 Ref/theories: added init_thy_reader and removed extend_theory. |
27 Tactics |
27 |
28 |
28 Ref/defining: type constraints ("::") now have a very low priority of 4. |
29 page 85: subgoals_tac is another tactic, for multiple calls to subgoal_tac |
29 As in ML, they must be enclosed in paretheses most of the time. |
|
30 |
30 |
31 Ref/syntax (page 145?): deleted repeated "the" in "before the the .thy file" |
31 Theories |
32 |
32 |
33 Logics/ZF: **************** |
33 page 117: the three lines of ML shown can be abbreviated to just |
34 renamed mem_anti_sym and mem_anti_refl to mem_asym and mem_irrefl |
34 init_thy_reader(); |
35 renamed union_iff to Union_iff |
|
36 renamed power_set to Pow_iff |
|
37 DiffD2: now is really a destruction rule |
|
38 escaped braces in qconverse_def, QSigma_def, lfp_def, gfp_def |
|
39 |
35 |
|
36 page 118: extend_theory has been replaced by numerous functions for adding |
|
37 types, constants, axioms, etc. |
|
38 |
|
39 Defining Logics |
|
40 |
|
41 page 127: type constraints ("::") now have a very low priority of 4. |
|
42 As in ML, they must usually be enclosed in paretheses. |
|
43 |
|
44 Syntax Transformations |
|
45 |
|
46 page 145, line -5: delete repeated "the" in "before the the .thy file" |
|
47 |
|
48 |
|
49 ISABELLE'S OBJECT-LOGICS |
|
50 |
|
51 Zermelo-Fraenkel Set Theory |
|
52 |
|
53 page 209: axioms have been renamed: |
|
54 union_iff is now Union_iff |
|
55 power_set is now Pow_iff |
|
56 |
|
57 page 215, bottom of figure 17.10: DiffD2 is now "c : A - B ==> c ~: B" |
|
58 |
|
59 page 215, bottom: rules mem_anti_sym and mem_anti_refl are now mem_asym and |
|
60 mem_irrefl |
|
61 |
|
62 page 222, top: missing braces in qconverse_def (around right-hand side) |
|
63 and QSigma_def (around <x;y>) |
|
64 |
|
65 page 223, top: lfp_def, gfp_def have missing braces around the argument of |
|
66 Inter, Union |
|
67 |
|
68 page 228: now there is also a theory of cardinal numbers and some |
|
69 developments involving the Axiom of Choice. |
|
70 |
|
71 page 229: now there is another examples directory, IMP (a semantics |
|
72 equivalence proof for an imperative language) |
|
73 |
|
74 Higher-Order Logic |
|
75 |
|
76 page 243: Pow is a new constant of type 'a set => 'a set set |
|
77 |
|
78 page 246: Pow is defined by Pow(A) == {B. B <= A} |
|
79 |
|
80 page 248: Pow has the rules |
|
81 PowI A<=B ==> A: Pow(B) |
|
82 PowD A: Pow(B) ==> A<=B |
|
83 |
|
84 page 259: HOL theory files may now include datatype declarations and |
|
85 (co)inductive definitions. (Two sections added.) |
|
86 |
|
87 page 259: now there is another examples directory, IMP (a semantics |
|
88 equivalence proof for an imperative language) |