* HOL: removed obsolete expand_if = split_if; theorems if_splits =
authorwenzelm
Tue Jul 18 21:08:20 2000 +0200 (2000-07-18)
changeset 9383c21fa1c48de0
parent 9382 7cea1cb9703e
child 9384 8e8941c491e6
* HOL: removed obsolete expand_if = split_if; theorems if_splits =
split_if split_if_asm; datatype package provides theorems foo.splits =
foo.split foo.split_asm for each datatype;
NEWS
     1.1 --- a/NEWS	Tue Jul 18 14:52:30 2000 +0200
     1.2 +++ b/NEWS	Tue Jul 18 21:08:20 2000 +0200
     1.3 @@ -33,6 +33,8 @@
     1.4  * HOL: theory Sexp now in HOL/Induct examples (used to be part of main
     1.5  HOL, but was unused); should better use HOL's datatype package anyway;
     1.6  
     1.7 +* HOL: removed obsolete theorem binding expand_if, use split_if instead;
     1.8 +
     1.9  * HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.10  
    1.11  * HOL/ML: even fewer consts are declared as global (see theories Ord,
    1.12 @@ -140,6 +142,10 @@
    1.13  * HOL/Calculation: new rules for substitution in inequalities
    1.14  (monotonicity conditions are extracted to be proven terminally);
    1.15  
    1.16 +* HOL: removed obsolete expand_if = split_if; theorems if_splits =
    1.17 +split_if split_if_asm; datatype package provides theorems foo.splits =
    1.18 +foo.split foo.split_asm for each datatype;
    1.19 +
    1.20  * names of theorems etc. may be natural numbers as well;
    1.21  
    1.22  * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;