--- a/NEWS Sun Feb 21 23:05:37 2010 +0100
+++ b/NEWS Mon Feb 22 09:17:49 2010 +0100
@@ -52,6 +52,12 @@
*** HOL ***
+* Multisets: changed orderings:
+ * pointwise ordering is instance of class order with standard syntax <= and <;
+ * multiset ordering has syntax <=# and <#; partial order properties are provided
+ by means of interpretation with prefix multiset_order.
+INCOMPATIBILITY.
+
* New set of rules "ac_simps" provides combined assoc / commute rewrites
for all interpretations of the appropriate generic locales.
@@ -63,7 +69,7 @@
* Some generic constants have been put to appropriate theories:
less_eq, less: Orderings
- abs, sgn: Groups
+ zero, one, plus, minus, uminus, times, abs, sgn: Groups
inverse, divide: Rings
INCOMPATIBILITY.
@@ -123,8 +129,7 @@
INCOMPATIBILITY.
* New theory Algebras contains generic algebraic structures and
-generic algebraic operations. INCOMPATIBILTY: constants zero, one,
-plus, minus, uminus and times have been moved from HOL.thy to Algebras.thy.
+generic algebraic operations.
* HOLogic.strip_psplit: types are returned in syntactic order, similar
to other strip and tuple operations. INCOMPATIBILITY.
@@ -133,10 +138,11 @@
replaced by new-style primrec, especially in theory List. The corresponding
constants now have authentic syntax. INCOMPATIBILITY.
-* Reorganized theory Multiset: less duplication, less historical
-organization of sections, conversion from associations lists to
-multisets, rudimentary code generation. Use insert_DiffM2 [symmetric]
-instead of elem_imp_eq_diff_union, if needed. INCOMPATIBILITY.
+* Reorganized theory Multiset: swapped notation of pointwise and multiset
+order; less duplication, less historical organization of sections,
+conversion from associations lists to multisets, rudimentary code generation.
+Use insert_DiffM2 [symmetric] instead of elem_imp_eq_diff_union, if needed.
+INCOMPATIBILITY.
* Reorganized theory Sum_Type; Inl and Inr now have authentic syntax.
INCOMPATIBILITY.