NEWS
changeset 4930 89271bc4e7ed
parent 4915 5ff99bd60da9
child 4981 9703ba0e9122
     1.1 --- a/NEWS	Thu May 14 16:44:04 1998 +0200
     1.2 +++ b/NEWS	Thu May 14 16:50:09 1998 +0200
     1.3 @@ -97,8 +97,8 @@
     1.4    remove it in a specific call of the simplifier using
     1.5    `... delsplits [split_if]'.
     1.6    You can also add/delete other case splitting rules to/from the default
     1.7 -  simpset: every datatype generates a suitable rule `split_t_case' (where t
     1.8 -  is the name of the datatype).
     1.9 +  simpset: every datatype generates suitable rules `split_t_case' and
    1.10 +  `split_t_case_asm' (where t is the name of the datatype).
    1.11  
    1.12  * new theory Vimage (inverse image of a function, syntax f-``B);
    1.13  
    1.14 @@ -267,19 +267,16 @@
    1.15         (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
    1.16       )
    1.17  
    1.18 -  which can be added to a simpset via `addsplits'. The existing theorems
    1.19 -  expand_list_case and expand_option_case have been renamed to
    1.20 -  split_list_case and split_option_case.
    1.21 -
    1.22 -  Additionally, there is a theorem `split_t_case_asm' of the form
    1.23 +  and a theorem `split_t_case_asm' of the form
    1.24  
    1.25    P(t_case f1 ... fn x) =
    1.26      ~( (? y1 ... ym1. x = C1 y1 ... ym1 & ~P(f1 y1 ... ym1)) |
    1.27          ...
    1.28         (? y1 ... ymn. x = Cn y1 ... ymn & ~P(f1 y1 ... ymn))
    1.29       )
    1.30 -
    1.31 -  it be used with the new `split_asm_tac'.
    1.32 +  which can be added to a simpset via `addsplits'. The existing theorems
    1.33 +  expand_list_case and expand_option_case have been renamed to
    1.34 +  split_list_case and split_option_case.
    1.35  
    1.36  * HOL/Arithmetic:
    1.37    - `pred n' is automatically converted to `n-1'.