NEWS
 changeset 4207 061919f8da9c parent 4189 b8c7a6bc6c16 child 4269 a045600f0c98
```     1.1 --- a/NEWS	Wed Nov 12 12:34:43 1997 +0100
1.2 +++ b/NEWS	Wed Nov 12 12:38:12 1997 +0100
1.3 @@ -95,7 +95,7 @@
1.4
1.5  *** HOL ***
1.6
1.7 -* HOL: there is a new splitter `split_prem_tac' that can be used e.g.
1.8 +* HOL: there is a new splitter `split_asm_tac' that can be used e.g.
1.9    with `addloop' of the simplifier to faciliate case splitting in premises.
1.10
1.11  * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
1.12 @@ -131,7 +131,7 @@
1.13    expand_list_case and expand_option_case have been renamed to
1.14    split_list_case and split_option_case.
1.15
1.16 -  Additionally, there is a theorem `split_t_case_prem' of the form
1.17 +  Additionally, there is a theorem `split_t_case_asm' of the form
1.18
1.19    P(t_case f1 ... fn x) =
1.20      ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
1.21 @@ -139,7 +139,7 @@
1.22         (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
1.23       )
1.24
1.25 -  it be used with the new `split_prem_tac'.
1.26 +  it be used with the new `split_asm_tac'.
1.27
1.28  * HOL/Lists: the function "set_of_list" has been renamed "set"
1.29    (and its theorems too);
1.30 @@ -175,7 +175,7 @@
1.31
1.32  *** FOL and ZF ***
1.33
1.34 -* FOL: there is a new splitter `split_prem_tac' that can be used e.g.
1.35 +* FOL: there is a new splitter `split_asm_tac' that can be used e.g.
1.36    with `addloop' of the simplifier to faciliate case splitting in premises.
1.37
1.38  * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
```