# HG changeset patch
# User nipkow
# Date 889196296 -3600
# Node ID de426efe87d3218041f641e03198d9e7bb1858fe
# Parent  ff081854fc863e3fe0370db074ade13fbc7232c7
*** empty log message ***

diff -r ff081854fc86 -r de426efe87d3 NEWS
--- a/NEWS	Fri Mar 06 15:20:29 1998 +0100
+++ b/NEWS	Fri Mar 06 15:58:16 1998 +0100
@@ -5,6 +5,10 @@
 New in Isabelle??? (FIXME)
 --------------------------
 
+* Rewrite rules for case distinctions can now be added permanently to the
+  default simpset using Addsplits just like Addsimps. They can be removed via
+  Delsplits just like Delsimps. For applications see HOL below.
+
 * changed wrapper mechanism for the classical reasoner now allows for selected
   deletion of wrappers, by introduction of names for wrapper functionals.
   This implies that addbefore, addSbefore, addaltern, and addSaltern now take
@@ -17,6 +21,16 @@
 
 *** HOL ***
 
+* The rule expand_if is now part of the default simpset. This means that
+  the simplifier will eliminate all ocurrences of if-then-else in the
+  conclusion of a goal. To prevent this, you can either remove expand_if
+  completely from the default simpset by `Delsplits [expand_if]' or
+  remove it in a specific call of the simplifier using
+  `... delsplits [expand_if]'.
+  You can also add/delete other case splitting rules to/from the default
+  simpset: every datatype generates a suitable rule `split_t_case' (where t
+  is the name of the datatype).
+
 * New theory Vimage (inverse image of a function, syntax f-``B)
 
 * Many new identities for unions, intersections, etc.