# HG changeset patch
# User oheimb
# Date 893409759 -7200
# Node ID df8fc4626a9ec432c0c080c3232552a1eb058471
# Parent  588538fb9308267e06bfb8d7c40a37e7d58e31f2
*** empty log message ***

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