diff -r 1025a27b08f9 -r b8c7a6bc6c16 NEWS
--- a/NEWS	Fri Nov 07 18:02:15 1997 +0100
+++ b/NEWS	Fri Nov 07 18:05:25 1997 +0100
@@ -95,6 +95,9 @@
 
 *** HOL ***
 
+* HOL: there is a new splitter `split_prem_tac' that can be used e.g. 
+  with `addloop' of the simplifier to faciliate case splitting in premises.
+
 * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
 
 * HOL/Auth: new protocol proofs including some for the Internet
@@ -121,13 +124,23 @@
   P(t_case f1 ... fn x) =
      ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
         ...
-        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
+       (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
      )
 
   which can be added to a simpset via `addsplits'. The existing theorems
   expand_list_case and expand_option_case have been renamed to
   split_list_case and split_option_case.
 
+  Additionally, there is a theorem `split_t_case_prem' of the form
+
+  P(t_case f1 ... fn x) =
+    ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
+        ...
+       (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
+     )
+
+  it be used with the new `split_prem_tac'.
+
 * HOL/Lists: the function "set_of_list" has been renamed "set"
   (and its theorems too);
 
@@ -162,6 +175,9 @@
 
 *** FOL and ZF ***
 
+* FOL: there is a new splitter `split_prem_tac' that can be used e.g. 
+  with `addloop' of the simplifier to faciliate case splitting in premises.
+
 * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
 in HOL, they strip ALL and --> from proved theorems;