5 New in Isabelle??? (FIXME) |
5 New in Isabelle??? (FIXME) |
6 -------------------------- |
6 -------------------------- |
7 |
7 |
8 * Rewrite rules for case distinctions can now be added permanently to the |
8 * Rewrite rules for case distinctions can now be added permanently to the |
9 default simpset using Addsplits just like Addsimps. They can be removed via |
9 default simpset using Addsplits just like Addsimps. They can be removed via |
10 Delsplits just like Delsimps. For applications see HOL below. |
10 Delsplits just like Delsimps. Lower-case versions are also available. |
|
11 For applications see HOL below. |
11 |
12 |
12 * Changed wrapper mechanism for the classical reasoner now allows for selected |
13 * Changed wrapper mechanism for the classical reasoner now allows for selected |
13 deletion of wrappers, by introduction of names for wrapper functionals. |
14 deletion of wrappers, by introduction of names for wrapper functionals. |
14 This implies that addbefore, addSbefore, addaltern, and addSaltern now take |
15 This implies that addbefore, addSbefore, addaltern, and addSaltern now take |
15 a pair (name, tactic) as argument, and that adding two tactics with the same |
16 a pair (name, tactic) as argument, and that adding two tactics with the same |
22 |
23 |
23 *** HOL *** |
24 *** HOL *** |
24 |
25 |
25 * HOL/Arithmetic: removed 'pred' (predecessor) function; |
26 * HOL/Arithmetic: removed 'pred' (predecessor) function; |
26 |
27 |
27 * The rule expand_if is now part of the default simpset. This means that |
28 * Simplifier: |
|
29 |
|
30 -The rule expand_if is now part of the default simpset. This means that |
28 the simplifier will eliminate all ocurrences of if-then-else in the |
31 the simplifier will eliminate all ocurrences of if-then-else in the |
29 conclusion of a goal. To prevent this, you can either remove expand_if |
32 conclusion of a goal. To prevent this, you can either remove expand_if |
30 completely from the default simpset by `Delsplits [expand_if]' or |
33 completely from the default simpset by `Delsplits [expand_if]' or |
31 remove it in a specific call of the simplifier using |
34 remove it in a specific call of the simplifier using |
32 `... delsplits [expand_if]'. |
35 `... delsplits [expand_if]'. |
33 You can also add/delete other case splitting rules to/from the default |
36 You can also add/delete other case splitting rules to/from the default |
34 simpset: every datatype generates a suitable rule `split_t_case' (where t |
37 simpset: every datatype generates a suitable rule `split_t_case' (where t |
35 is the name of the datatype). |
38 is the name of the datatype). |
|
39 |
|
40 -Asm_full_simp_tac is now more aggressive: |
|
41 1. It will sometimes reorient premises if that increases their power to |
|
42 simplify. |
|
43 2. It does no longer proceed strictly from left to right but may also |
|
44 rotate premises to achieve further simplification. |
|
45 For compatibility reasons there is now Asm_lr_simp_tac which is like the |
|
46 old Asm_full_simp_tac in that it does not rotate premises. |
36 |
47 |
37 * new theory Vimage (inverse image of a function, syntax f-``B); |
48 * new theory Vimage (inverse image of a function, syntax f-``B); |
38 |
49 |
39 * many new identities for unions, intersections, etc.; |
50 * many new identities for unions, intersections, etc.; |
40 |
51 |