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 n1 
44 some theorems about n1 