1.1 --- a/NEWS	Wed Apr 22 19:09:44 1998 +0200
     1.2 +++ b/NEWS	Fri Apr 24 11:22:39 1998 +0200
     1.3 @@ -15,9 +15,10 @@
     1.4    This implies that addbefore, addSbefore, addaltern, and addSaltern now take
     1.5    a pair (name, tactic) as argument, and that adding two tactics with the same
     1.6    name overwrites the first one (emitting a warning).
     1.7 +  type wrapper = (int -> tactic) -> (int -> tactic)
     1.8    setWrapper, setSWrapper, compWrapper and compSWrapper are replaced by
     1.9 -  addWrapper, addSWrapper: claset * wrapper -> claset
    1.10 -  delWrapper, delSWrapper: claset *  string -> claset
    1.11 +  addWrapper, addSWrapper: claset * (string * wrapper) -> claset
    1.12 +  delWrapper, delSWrapper: claset *  string            -> claset
    1.13    getWrapper is renamed to appWrappers, getSWrapper to appSWrappers;
    1.14  
    1.15  * Inductive definitions now handle disjunctive premises correctly (HOL and ZF)
    1.16 @@ -25,11 +26,17 @@
    1.17  
    1.18  *** HOL ***
    1.19  
    1.20 +* new force_tac (and its derivations Force_tac, force) 
    1.21 +  combines rewriting and classical reasoning (and whatever other tools)
    1.22 +  similarly to auto_tac, but is aimed to solve the given subgoal totally.
    1.23 +
    1.24  * added option_map_eq_Some to simpset(), option_map_eq_Some RS iffD1 to claset()
    1.25  * New directory HOL/UNITY: Chandy and Misra's UNITY formalism
    1.26  
    1.27 -* split_all_tac now fails if there is nothing to split
    1.28 -  split_all_tac has moved within claset() from usafe wrappers to safe wrappers
    1.29 +* split_all_tac is now much faster and fails if there is nothing to split
    1.30 +  split_all_tac has moved within claset() from usafe wrappers to safe wrappers,
    1.31 +  which means that !!-bound variables are splitted much more aggressively.
    1.32 +  If this splitting is not appropriate, use delSWrapper "split_all_tac".
    1.33  
    1.34  * added disj_not1 = "(~P | Q) = (P --> Q)" to the default simpset
    1.35