NEWS
changeset 37591 d3daea901123
parent 37536 c62aa9281101
child 37608 165cd386288d
--- a/NEWS	Mon Jun 28 15:03:07 2010 +0200
+++ b/NEWS	Mon Jun 28 15:03:07 2010 +0200
@@ -17,6 +17,10 @@
 
 *** HOL ***
 
+* Constant "split" has been merged with constant "prod_case";  names
+of ML functions, facts etc. involving split have been retained so far,
+though.  INCOMPATIBILITY.
+
 * Some previously unqualified names have been qualified:
 
   types