consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
authorhaftmann
Fri, 06 Jan 2012 21:48:45 +0100
changeset 46145 0ec0af1c651d
parent 46144 cc374091999b
child 46146 6baea4fca6bd
consolidated various theorem names relating to Finite_Set.fold and List.fold combinators
NEWS
--- a/NEWS	Fri Jan 06 20:48:52 2012 +0100
+++ b/NEWS	Fri Jan 06 21:48:45 2012 +0100
@@ -60,6 +60,16 @@
 
 *** HOL ***
 
+* Consolidated various theorem names relating to Finite_Set.fold combinator:
+  inf_INFI_fold_inf ~> inf_INF_fold_inf
+  sup_SUPR_fold_sup ~> sup_SUP_fold_sup
+  INFI_fold_inf ~> INF_fold_inf
+  SUPR_fold_sup ~> SUP_fold_sup
+  union_set ~> union_set_fold
+  minus_set ~> minus_set_fold
+  
+INCOMPATIBILITY.
+
 * Consolidated theorem names concerning fold combinators:
   INFI_set_fold ~> INF_set_fold
   SUPR_set_fold ~> SUP_set_fold