equal
deleted
inserted
replaced
52 |
52 |
53 * Pure: fixed 'token_translation' command; |
53 * Pure: fixed 'token_translation' command; |
54 |
54 |
55 * Pure: removed obsolete 'exported' attribute; |
55 * Pure: removed obsolete 'exported' attribute; |
56 |
56 |
57 * Pure: dummy pattern "_" in is/let is now automatically ``lifted'' |
57 * Pure: dummy pattern "_" in is/let is now automatically lifted over |
58 over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") |
58 bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") |
59 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x"); |
59 supersedes more cumbersome ... (is "ALL x. _ x --> ?C x"); |
60 |
60 |
61 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms; |
61 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms; |
62 |
62 |
63 * HOL: 'recdef' now fails on unfinished automated proofs, use |
63 * HOL: 'recdef' now fails on unfinished automated proofs, use |
64 "(permissive)" option to recover old behavior; |
64 "(permissive)" option to recover old behavior; |
65 |
65 |
66 * HOL: 'inductive' now longer features separate (collective) |
66 * HOL: 'inductive' no longer features separate (collective) attributes |
67 attributes for 'intros'; |
67 for 'intros' (was found too confusing); |
68 |
68 |
69 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); |
|
70 |
69 |
71 |
70 |
72 *** HOL *** |
71 *** HOL *** |
73 |
72 |
74 * HOL: moved over to sane numeral syntax; the new policy is as |
73 * HOL: moved over to sane numeral syntax; the new policy is as |
97 |
96 |
98 - remove all special provisions on numerals in proofs; |
97 - remove all special provisions on numerals in proofs; |
99 |
98 |
100 * HOL/record: |
99 * HOL/record: |
101 - provides cases/induct rules for use with corresponding Isar methods; |
100 - provides cases/induct rules for use with corresponding Isar methods; |
102 - "record" operation truncates to particular fixed record (acts like |
101 - "record" operation truncates to particular fixed record (type cast); |
103 a type cast); |
102 - make_defs no longer part of default simps (INCOMPATIBILITY); |
104 - make_defs no longer part of default simps; |
|
105 - internal definitions directly based on a light-weight abstract |
103 - internal definitions directly based on a light-weight abstract |
106 theory of product types over typedef rather than datatype; |
104 theory of product types over typedef rather than datatype; |
|
105 |
|
106 * HOL: canonical cases/induct rules for n-tuples (n = 3..7); |
107 |
107 |
108 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" |
108 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" |
109 (beware of argument permutation!); |
109 (beware of argument permutation!); |
110 |
110 |
111 * HOL: linorder_less_split superseded by linorder_cases; |
111 * HOL: linorder_less_split superseded by linorder_cases; |
131 expressions; |
131 expressions; |
132 |
132 |
133 * HOL/GroupTheory: group theory examples including Sylow's theorem, by |
133 * HOL/GroupTheory: group theory examples including Sylow's theorem, by |
134 Florian Kammüller; |
134 Florian Kammüller; |
135 |
135 |
136 * HOL: eliminated global items |
136 * HOL: got rid of some global declarations (potential INCOMPATIBILITY |
137 |
137 for ML tools): const "()" renamed "Product_Type.Unity", type "unit" |
138 const "()" -> "Product_Type.Unity" |
138 renamed "Product_Type.unit"; |
139 type "unit" -> "Product_Type.unit" |
|
140 |
139 |
141 |
140 |
142 *** ZF *** |
141 *** ZF *** |
143 |
142 |
144 * ZF: the integer library now covers quotients and remainders, with |
143 * ZF: the integer library now covers quotients and remainders, with |