# HG changeset patch
# User oheimb
# Date 879334692 -3600
# Node ID 061919f8da9c99455ae44e997d4e02fa0470d293
# Parent  688050e83d890fa81aea282bfc1347003aba7f55
renamed split_prem_tac to split_asm_tac

diff -r 688050e83d89 -r 061919f8da9c NEWS
--- a/NEWS	Wed Nov 12 12:34:43 1997 +0100
+++ b/NEWS	Wed Nov 12 12:38:12 1997 +0100
@@ -95,7 +95,7 @@
 
 *** HOL ***
 
-* HOL: there is a new splitter `split_prem_tac' that can be used e.g. 
+* HOL: there is a new splitter `split_asm_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;
@@ -131,7 +131,7 @@
   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
+  Additionally, there is a theorem `split_t_case_asm' of the form
 
   P(t_case f1 ... fn x) =
     ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
@@ -139,7 +139,7 @@
        (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
      )
 
-  it be used with the new `split_prem_tac'.
+  it be used with the new `split_asm_tac'.
 
 * HOL/Lists: the function "set_of_list" has been renamed "set"
   (and its theorems too);
@@ -175,7 +175,7 @@
 
 *** FOL and ZF ***
 
-* FOL: there is a new splitter `split_prem_tac' that can be used e.g. 
+* FOL: there is a new splitter `split_asm_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