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. For applications see HOL below. |
11 |
11 |
12 * changed wrapper mechanism for the classical reasoner now allows for selected |
12 * Changed wrapper mechanism for the classical reasoner now allows for selected |
13 deletion of wrappers, by introduction of names for wrapper functionals. |
13 deletion of wrappers, by introduction of names for wrapper functionals. |
14 This implies that addbefore, addSbefore, addaltern, and addSaltern now take |
14 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 |
15 a pair (name, tactic) as argument, and that adding two tactics with the same |
16 name overwrites the first one (emitting a warning). |
16 name overwrites the first one (emitting a warning). |
17 setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by |
17 setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by |
18 addWrapper, addSWrapper: claset * wrapper -> claset |
18 addWrapper, addSWrapper: claset * wrapper -> claset |
19 delWrapper, delSWrapper: claset * string -> claset |
19 delWrapper, delSWrapper: claset * string -> claset |
20 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
20 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
21 |
21 |
|
22 |
22 *** HOL *** |
23 *** HOL *** |
|
24 |
|
25 * HOL/Arithmetic: removed 'pred' (predecessor) function; |
23 |
26 |
24 * The rule expand_if is now part of the default simpset. This means that |
27 * The rule expand_if is now part of the default simpset. This means that |
25 the simplifier will eliminate all ocurrences of if-then-else in the |
28 the simplifier will eliminate all ocurrences of if-then-else in the |
26 conclusion of a goal. To prevent this, you can either remove expand_if |
29 conclusion of a goal. To prevent this, you can either remove expand_if |
27 completely from the default simpset by `Delsplits [expand_if]' or |
30 completely from the default simpset by `Delsplits [expand_if]' or |
29 `... delsplits [expand_if]'. |
32 `... delsplits [expand_if]'. |
30 You can also add/delete other case splitting rules to/from the default |
33 You can also add/delete other case splitting rules to/from the default |
31 simpset: every datatype generates a suitable rule `split_t_case' (where t |
34 simpset: every datatype generates a suitable rule `split_t_case' (where t |
32 is the name of the datatype). |
35 is the name of the datatype). |
33 |
36 |
34 * New theory Vimage (inverse image of a function, syntax f-``B) |
37 * new theory Vimage (inverse image of a function, syntax f-``B); |
35 |
38 |
36 * Many new identities for unions, intersections, etc. |
39 * many new identities for unions, intersections, etc.; |
|
40 |
37 |
41 |
38 |
42 |
39 New in Isabelle98 (January 1998) |
43 New in Isabelle98 (January 1998) |
40 -------------------------------- |
44 -------------------------------- |
41 |
45 |