# HG changeset patch
# User wenzelm
# Date 963947300 -7200
# Node ID c21fa1c48de0a2671a898d3a4e8f43e70101e7ac
# Parent  7cea1cb9703e40c8859c2eea818acaeada3f2ad5
* 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;

diff -r 7cea1cb9703e -r c21fa1c48de0 NEWS
--- a/NEWS	Tue Jul 18 14:52:30 2000 +0200
+++ b/NEWS	Tue Jul 18 21:08:20 2000 +0200
@@ -33,6 +33,8 @@
 * HOL: theory Sexp now in HOL/Induct examples (used to be part of main
 HOL, but was unused); should better use HOL's datatype package anyway;
 
+* HOL: removed obsolete theorem binding expand_if, use split_if instead;
+
 * HOL/Real: "rabs" replaced by overloaded "abs" function;
 
 * HOL/ML: even fewer consts are declared as global (see theories Ord,
@@ -140,6 +142,10 @@
 * HOL/Calculation: new rules for substitution in inequalities
 (monotonicity conditions are extracted to be proven terminally);
 
+* 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;
+
 * names of theorems etc. may be natural numbers as well;
 
 * Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;