36 page 118: extend_theory has been replaced by numerous functions for adding |
36 page 118: extend_theory has been replaced by numerous functions for adding |
37 types, constants, axioms, etc. |
37 types, constants, axioms, etc. |
38 |
38 |
39 Defining Logics |
39 Defining Logics |
40 |
40 |
|
41 |
|
42 |
41 page 127: type constraints ("::") now have a very low priority of 4. |
43 page 127: type constraints ("::") now have a very low priority of 4. |
42 As in ML, they must usually be enclosed in paretheses. |
44 As in ML, they must usually be enclosed in paretheses. |
43 |
45 |
44 Syntax Transformations |
46 Syntax Transformations |
45 |
47 |
46 page 145, line -5: delete repeated "the" in "before the the .thy file" |
48 page 145, line -5: delete repeated "the" in "before the the .thy file" |
47 |
49 |
48 Simplification |
50 Simplification |
49 |
51 |
|
52 page 157 display: Union operator is too big |
|
53 |
50 page 158, "!": Isabelle now permits more general left-hand sides, so called |
54 page 158, "!": Isabelle now permits more general left-hand sides, so called |
51 higher-order patterns. |
55 higher-order patterns. |
52 |
56 |
|
57 |
53 ISABELLE'S OBJECT-LOGICS |
58 ISABELLE'S OBJECT-LOGICS |
54 |
59 |
|
60 First-Order Logic |
|
61 |
|
62 page 191: FOL_dup_cs is now deleted (use deepen_tac FOL_cs instead) |
|
63 |
55 Zermelo-Fraenkel Set Theory |
64 Zermelo-Fraenkel Set Theory |
|
65 |
|
66 page 204: type i has class term, not (just) logic |
56 |
67 |
57 page 209: axioms have been renamed: |
68 page 209: axioms have been renamed: |
58 union_iff is now Union_iff |
69 union_iff is now Union_iff |
59 power_set is now Pow_iff |
70 power_set is now Pow_iff |
60 |
71 |
89 Definition modified accordingly |
100 Definition modified accordingly |
90 |
101 |
91 page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c |
102 page 252: sum_case now has type ['a=>'c,'b=>'c, 'a+'b] =>'c |
92 Definition and rules modified accordingly |
103 Definition and rules modified accordingly |
93 |
104 |
|
105 page 252: HOL_dup_cs is now deleted (use deepen_tac HOL_cs instead) |
|
106 |
94 page 254: nat_case now has type ['a, nat=>'a, nat] =>'a |
107 page 254: nat_case now has type ['a, nat=>'a, nat] =>'a |
95 Definition modified accordingly |
108 Definition modified accordingly |
96 |
109 |
97 page 256,258: list_case now takes the list as its last argument, not the |
110 page 256,258: list_case now takes the list as its last argument, not the |
98 first. |
111 first. |