NEWS
changeset 4189 b8c7a6bc6c16
parent 4178 e64ff1c1bc70
child 4207 061919f8da9c
     1.1 --- a/NEWS	Fri Nov 07 18:02:15 1997 +0100
     1.2 +++ b/NEWS	Fri Nov 07 18:05:25 1997 +0100
     1.3 @@ -95,6 +95,9 @@
     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 +  with `addloop' of the simplifier to faciliate case splitting in premises.
     1.9 +
    1.10  * HOL/TLA: Stephan Merz's formalization of Lamport's Temporal Logic of Actions;
    1.11  
    1.12  * HOL/Auth: new protocol proofs including some for the Internet
    1.13 @@ -121,13 +124,23 @@
    1.14    P(t_case f1 ... fn x) =
    1.15       ( (!y1 ... ym1. x = C1 y1 ... ym1 --> P(f1 y1 ... ym1)) &
    1.16          ...
    1.17 -        (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
    1.18 +       (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
    1.19       )
    1.20  
    1.21    which can be added to a simpset via `addsplits'. The existing theorems
    1.22    expand_list_case and expand_option_case have been renamed to
    1.23    split_list_case and split_option_case.
    1.24  
    1.25 +  Additionally, there is a theorem `split_t_case_prem' of the form
    1.26 +
    1.27 +  P(t_case f1 ... fn x) =
    1.28 +    ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
    1.29 +        ...
    1.30 +       (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
    1.31 +     )
    1.32 +
    1.33 +  it be used with the new `split_prem_tac'.
    1.34 +
    1.35  * HOL/Lists: the function "set_of_list" has been renamed "set"
    1.36    (and its theorems too);
    1.37  
    1.38 @@ -162,6 +175,9 @@
    1.39  
    1.40  *** FOL and ZF ***
    1.41  
    1.42 +* FOL: there is a new splitter `split_prem_tac' that can be used e.g. 
    1.43 +  with `addloop' of the simplifier to faciliate case splitting in premises.
    1.44 +
    1.45  * qed_spec_mp, qed_goal_spec_mp, qed_goalw_spec_mp are available, as
    1.46  in HOL, they strip ALL and --> from proved theorems;
    1.47