4 |
4 |
5 New in Isabelle??? (FIXME) |
5 New in Isabelle??? (FIXME) |
6 -------------------------- |
6 -------------------------- |
7 |
7 |
8 *** General Changes *** |
8 *** General Changes *** |
|
9 |
|
10 * Simplifier: |
|
11 |
|
12 -Asm_full_simp_tac is now more aggressive: |
|
13 1. It will sometimes reorient premises if that increases their power to |
|
14 simplify. |
|
15 2. It does no longer proceed strictly from left to right but may also |
|
16 rotate premises to achieve further simplification. |
|
17 For compatibility reasons there is now Asm_lr_simp_tac which is like the |
|
18 old Asm_full_simp_tac in that it does not rotate premises. |
9 |
19 |
10 * Changed wrapper mechanism for the classical reasoner now allows for |
20 * Changed wrapper mechanism for the classical reasoner now allows for |
11 selected deletion of wrappers, by introduction of names for wrapper |
21 selected deletion of wrappers, by introduction of names for wrapper |
12 functionals. This implies that addbefore, addSbefore, addaltern, and |
22 functionals. This implies that addbefore, addSbefore, addaltern, and |
13 addSaltern now take a pair (name, tactic) as argument, and that adding |
23 addSaltern now take a pair (name, tactic) as argument, and that adding |
62 instead of "inverse"; |
72 instead of "inverse"; |
63 |
73 |
64 * recdef can now declare non-recursive functions, with {} supplied as |
74 * recdef can now declare non-recursive functions, with {} supplied as |
65 the well-founded relation; |
75 the well-founded relation; |
66 |
76 |
|
77 * expand_if, expand_split, expand_sum_case and expand_nat_case are now called |
|
78 split_if, split_split, split_sum_case and split_nat_case |
|
79 (to go with add/delsplits). |
|
80 |
67 * Simplifier: |
81 * Simplifier: |
68 |
82 |
69 -Rewrite rules for case distinctions can now be added permanently to the |
83 -Rewrite rules for case distinctions can now be added permanently to the |
70 default simpset using Addsplits just like Addsimps. They can be removed via |
84 default simpset using Addsplits just like Addsimps. They can be removed via |
71 Delsplits just like Delsimps. Lower-case versions are also available. |
85 Delsplits just like Delsimps. Lower-case versions are also available. |
72 |
86 |
73 -The rule expand_if is now part of the default simpset. This means that |
87 -The rule split_if is now part of the default simpset. This means that |
74 the simplifier will eliminate all ocurrences of if-then-else in the |
88 the simplifier will eliminate all ocurrences of if-then-else in the |
75 conclusion of a goal. To prevent this, you can either remove expand_if |
89 conclusion of a goal. To prevent this, you can either remove split_if |
76 completely from the default simpset by `Delsplits [expand_if]' or |
90 completely from the default simpset by `Delsplits [split_if]' or |
77 remove it in a specific call of the simplifier using |
91 remove it in a specific call of the simplifier using |
78 `... delsplits [expand_if]'. |
92 `... delsplits [split_if]'. |
79 You can also add/delete other case splitting rules to/from the default |
93 You can also add/delete other case splitting rules to/from the default |
80 simpset: every datatype generates a suitable rule `split_t_case' (where t |
94 simpset: every datatype generates a suitable rule `split_t_case' (where t |
81 is the name of the datatype). |
95 is the name of the datatype). |
82 |
|
83 -Asm_full_simp_tac is now more aggressive: |
|
84 1. It will sometimes reorient premises if that increases their power to |
|
85 simplify. |
|
86 2. It does no longer proceed strictly from left to right but may also |
|
87 rotate premises to achieve further simplification. |
|
88 For compatibility reasons there is now Asm_lr_simp_tac which is like the |
|
89 old Asm_full_simp_tac in that it does not rotate premises. |
|
90 |
|
91 * expand_if, expand_split, expand_sum_case and expand_nat_case are now called |
|
92 split_if, split_split, split_sum_case and split_nat_case |
|
93 (to go with add/delsplits). |
|
94 |
96 |
95 * new theory Vimage (inverse image of a function, syntax f-``B); |
97 * new theory Vimage (inverse image of a function, syntax f-``B); |
96 |
98 |
97 * many new identities for unions, intersections, set difference, etc.; |
99 * many new identities for unions, intersections, set difference, etc.; |
98 |
100 |