fixed NEWS w.r.t. multisets
authorblanchet
Wed, 20 Jan 2016 18:04:41 +0100
changeset 62209 009c6e0b44bb
parent 62208 ad43b3ab06e4
child 62215 e208fa77beb1
fixed NEWS w.r.t. multisets
NEWS
--- a/NEWS	Wed Jan 20 17:14:53 2016 +0100
+++ b/NEWS	Wed Jan 20 18:04:41 2016 +0100
@@ -649,15 +649,16 @@
   - Renamed multiset inclusion operators:
       < ~> <#
       > ~> >#
-      \<subset> ~> \<subset>#
-      \<supset> ~> \<supset>#
       <= ~> <=#
       >= ~> >=#
       \<le> ~> \<le>#
       \<ge> ~> \<ge>#
-      \<subseteq> ~> \<subseteq>#
-      \<supseteq> ~> \<supseteq>#
     INCOMPATIBILITY.
+  - Added multiset inclusion operator syntax:
+      \<subset>#
+      \<subseteq>#
+      \<supset>#
+      \<supseteq>#
   - "'a multiset" is no longer an instance of the "order",
     "ordered_ab_semigroup_add_imp_le", "ordered_cancel_comm_monoid_diff",
     "semilattice_inf", and "semilattice_sup" type classes. The theorems