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