12 issue the following ML commands: |
12 issue the following ML commands: |
13 |
13 |
14 Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; |
14 Delsimprocs Nat_Numeral_Simprocs.cancel_numerals; |
15 Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; |
15 Delsimprocs [Nat_Numeral_Simprocs.combine_numerals]; |
16 |
16 |
17 * HOL: simplification no longer dives into case-expressions; |
17 * HOL: simplification no longer dives into case-expressions; this is |
|
18 controlled by "t.weak_case_cong" for each datatype t; |
18 |
19 |
19 * HOL: nat_less_induct renamed to less_induct; |
20 * HOL: nat_less_induct renamed to less_induct; |
20 |
21 |
21 * HOL: systematic renaming of the SOME (Eps) rules, may use isatool |
22 * HOL: systematic renaming of the SOME (Eps) rules, may use isatool |
22 fixsome to patch .thy and .ML sources automatically; |
23 fixsome to patch .thy and .ML sources automatically; |
273 * HOL: new version of "case_tac" subsumes both boolean case split and |
274 * HOL: new version of "case_tac" subsumes both boolean case split and |
274 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
275 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer |
275 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
276 exists, may define val exhaust_tac = case_tac for ad-hoc portability; |
276 |
277 |
277 * HOL: simplification no longer dives into case-expressions: only the |
278 * HOL: simplification no longer dives into case-expressions: only the |
278 selector expression is simplified, but not the remaining arms. To |
279 selector expression is simplified, but not the remaining arms; to |
279 enable full simplification of case-expressions for datatype t, you |
280 enable full simplification of case-expressions for datatype t, you may |
280 need to remove t.weak_case_cong from the simpset, either permanently |
281 remove t.weak_case_cong from the simpset, either globally (Delcongs |
281 (Delcongs [thm"t.weak_case_cong"];) or locally (delcongs [...]). |
282 [thm"t.weak_case_cong"];) or locally (delcongs [...]). |
282 |
283 |
283 * HOL/recdef: the recursion equations generated by 'recdef' for |
284 * HOL/recdef: the recursion equations generated by 'recdef' for |
284 function 'f' are now called f.simps instead of f.rules; if all |
285 function 'f' are now called f.simps instead of f.rules; if all |
285 termination conditions are proved automatically, these simplification |
286 termination conditions are proved automatically, these simplification |
286 rules are added to the simpset, as in primrec; rules may be named |
287 rules are added to the simpset, as in primrec; rules may be named |