10 |
10 |
11 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; |
11 * HOL: exhaust_tac on datatypes superceded by new generic case_tac; |
12 |
12 |
13 * HOL: simplification no longer dives into case-expressions |
13 * HOL: simplification no longer dives into case-expressions |
14 |
14 |
15 * HOL: the recursion equations generated by `recdef' are now called |
15 * HOL: the recursion equations generated by 'recdef' are now called |
16 f.simps instead of f.rules. |
16 f.simps instead of f.rules; |
17 |
17 |
18 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; |
18 * ML: PureThy.add_thms/add_axioms/add_defs return theorems as well; |
19 |
19 |
20 |
20 |
21 *** Document preparation *** |
21 *** Document preparation *** |
104 expression is simplified, but not the remaining arms. To enable full |
104 expression is simplified, but not the remaining arms. To enable full |
105 simplification of case-expressions for datatype t, you need to remove |
105 simplification of case-expressions for datatype t, you need to remove |
106 t.weak_case_cong from the simpset, either permanently |
106 t.weak_case_cong from the simpset, either permanently |
107 (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]). |
107 (Delcongs[thm"t.weak_case_cong"];) or locally (delcongs [...]). |
108 |
108 |
109 * the recursion equations generated by `recdef' for function `f' are now |
109 * the recursion equations generated by 'recdef' for function 'f' are |
110 called f.simps instead of f.rules. If all termination conditions are proved |
110 now called f.simps instead of f.rules; if all termination conditions |
111 automatically, these simplification rules are added to the simpset, as in |
111 are proved automatically, these simplification rules are added to the |
112 primrec. These simplification rules are numbered canonically: all equations |
112 simpset, as in primrec; rules may be named individually as well, |
113 generated from clauses i are called "f.i"; counting starts with 0. These |
113 resulting in a separate list of theorems for each equation; |
114 equations can be removed from the simpset like this: delsimps (thms"f.i"). |
|
115 |
114 |
116 |
115 |
117 *** General *** |
116 *** General *** |
118 |
117 |
119 * compression of ML heaps images may now be controlled via -c option |
118 * compression of ML heaps images may now be controlled via -c option |