NEWS
changeset 59986 f38b94549dc8
parent 59967 2fcf41a626f7
child 59991 09be0495dcc2
--- a/NEWS	Thu Apr 09 15:54:09 2015 +0200
+++ b/NEWS	Thu Apr 09 18:00:58 2015 +0200
@@ -338,6 +338,10 @@
       \<subset># ~> #\<subset>#
       \<subseteq># ~> #\<subseteq>#
     INCOMPATIBILITY.
+  - Introduced abbreviations for ill-named multiset operations:
+      <#, \<subset># abbreviate < (strict subset)
+      <=#, \<le>#, \<subseteq># abbreviate <= (subset or equal)
+    INCOMPATIBILITY.
   - Renamed
       in_multiset_of ~> in_multiset_in_set
     INCOMPATIBILITY.