# HG changeset patch
# User haftmann
# Date 1277996105 -7200
# Node ID 03217132b79254ac751bc7c9dcb6e20a1e2d4983
# Parent  0040bafffdef09e97a47986f5b912da10fb4314e
"prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect

diff -r 0040bafffdef -r 03217132b792 NEWS
--- a/NEWS	Thu Jul 01 16:54:44 2010 +0200
+++ b/NEWS	Thu Jul 01 16:55:05 2010 +0200
@@ -17,6 +17,9 @@
 
 *** HOL ***
 
+* Abolished symbol type names:  "prod" and "sum" replace "*" and "+"
+respectively.  INCOMPATBILITY.
+
 * Constant "split" has been merged with constant "prod_case";  names
 of ML functions, facts etc. involving split have been retained so far,
 though.  INCOMPATIBILITY.
@@ -41,8 +44,6 @@
 
   types
     nat ~> Nat.nat
-    * ~> Product_Type.*
-    + ~> Sum_Type.+
 
   constants
     Ball ~> Set.Ball
@@ -51,8 +52,9 @@
     Pair ~> Product_Type.Pair
     fst ~> Product_Type.fst
     snd ~> Product_Type.snd
-    split ~> Product_Type.split
     curry ~> Product_Type.curry
+    op : ~> Set.member
+    Collect ~> Set.Collect
 
 INCOMPATIBILITY.