# HG changeset patch
# User nipkow
# Date 878541395 -3600
# Node ID 3a6e1e562aede0bd0442cbcc10ad5b36d66d707a
# Parent  d6d06a03a2e9fe9a30cc38986e1cb3fd276e41d0
*** empty log message ***

diff -r d6d06a03a2e9 -r 3a6e1e562aed NEWS
--- a/NEWS	Mon Nov 03 08:08:14 1997 +0100
+++ b/NEWS	Mon Nov 03 08:16:35 1997 +0100
@@ -109,7 +109,9 @@
         (!y1 ... ymn. x = Cn y1 ... ymn --> P(f1 y1 ... ymn))
      )
 
-  which can be added to a simpset via `addsplits'.
+  which can be added to a simpset via `addsplits'. The existing theorems
+  expand_list_case and expand_option_case have been renamed to
+  split_list_case and split_option_case.
 
 * HOL/Lists: the function "set_of_list" has been renamed "set"
   (and its theorems too);