13 * Changed wrapper mechanism for the classical reasoner now allows for selected |
13 * Changed wrapper mechanism for the classical reasoner now allows for selected |
14 deletion of wrappers, by introduction of names for wrapper functionals. |
14 deletion of wrappers, by introduction of names for wrapper functionals. |
15 This implies that addbefore, addSbefore, addaltern, and addSaltern now take |
15 This implies that addbefore, addSbefore, addaltern, and addSaltern now take |
16 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 |
17 name overwrites the first one (emitting a warning). |
17 name overwrites the first one (emitting a warning). |
|
18 type wrapper = (int -> tactic) -> (int -> tactic) |
18 setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by |
19 setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by |
19 addWrapper, addSWrapper: claset * wrapper -> claset |
20 addWrapper, addSWrapper: claset * (string * wrapper) -> claset |
20 delWrapper, delSWrapper: claset * string -> claset |
21 delWrapper, delSWrapper: claset * string -> claset |
21 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
22 getWrapper is renamed to appWrappers, getSWrapper to appSWrappers; |
22 |
23 |
23 * Inductive definitions now handle disjunctive premises correctly (HOL and ZF) |
24 * Inductive definitions now handle disjunctive premises correctly (HOL and ZF) |
24 |
25 |
25 |
26 |
26 *** HOL *** |
27 *** HOL *** |
|
28 |
|
29 * new force_tac (and its derivations Force_tac, force) |
|
30 combines rewriting and classical reasoning (and whatever other tools) |
|
31 similarly to auto_tac, but is aimed to solve the given subgoal totally. |
27 |
32 |
28 * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset() |
33 * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset() |
29 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism |
34 * New directory HOL/UNITY: Chandy and Misra's UNITY formalism |
30 |
35 |
31 * split_all_tac now fails if there is nothing to split |
36 * split_all_tac is now much faster and fails if there is nothing to split |
32 split_all_tac has moved within claset() from usafe wrappers to safe wrappers |
37 split_all_tac has moved within claset() from usafe wrappers to safe wrappers, |
|
38 which means that !!-bound variables are splitted much more aggressively. |
|
39 If this splitting is not appropriate, use delSWrapper "split_all_tac". |
33 |
40 |
34 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset |
41 * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset |
35 |
42 |
36 * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized |
43 * HOL/Arithmetic: removed 'pred' (predecessor) function; and generalized |
37 some theorems about n-1 |
44 some theorems about n-1 |