switched notations for pointwise and multiset order

--- a/src/HOL/Algebra/Divisibility.thy	Mon Feb 22 09:15:10 2010 +0100
+++ b/src/HOL/Algebra/Divisibility.thy	Mon Feb 22 09:15:10 2010 +0100
@@ -2250,7 +2250,7 @@
   assumes ab: "a divides b"
     and afs: "wfactors G as a" and bfs: "wfactors G bs b"
     and carr: "a \<in> carrier G"  "b \<in> carrier G"  "set as \<subseteq> carrier G"  "set bs \<subseteq> carrier G"
-  shows "fmset G as \<le># fmset G bs"
+  shows "fmset G as \<le> fmset G bs"
 using ab
 proof (elim dividesE)
   fix c
@@ -2270,7 +2270,7 @@
 qed
 
 lemma (in comm_monoid_cancel) fmsubset_divides:
-  assumes msubset: "fmset G as \<le># fmset G bs"
+  assumes msubset: "fmset G as \<le> fmset G bs"
     and afs: "wfactors G as a" and bfs: "wfactors G bs b"
     and acarr: "a \<in> carrier G" and bcarr: "b \<in> carrier G"
     and ascarr: "set as \<subseteq> carrier G" and bscarr: "set bs \<subseteq> carrier G"
@@ -2323,7 +2323,7 @@
   assumes "wfactors G as a" and "wfactors G bs b"
     and "a \<in> carrier G" and "b \<in> carrier G" 
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
-  shows "a divides b = (fmset G as \<le># fmset G bs)"
+  shows "a divides b = (fmset G as \<le> fmset G bs)"
 using assms
 by (blast intro: divides_fmsubset fmsubset_divides)
 
@@ -2331,7 +2331,7 @@
 text {* Proper factors on multisets *}
 
 lemma (in factorial_monoid) fmset_properfactor:
-  assumes asubb: "fmset G as \<le># fmset G bs"
+  assumes asubb: "fmset G as \<le> fmset G bs"
     and anb: "fmset G as \<noteq> fmset G bs"
     and "wfactors G as a" and "wfactors G bs b"
     and "a \<in> carrier G" and "b \<in> carrier G"
@@ -2341,10 +2341,10 @@
 apply (rule fmsubset_divides[of as bs], fact+)
 proof
   assume "b divides a"
-  hence "fmset G bs \<le># fmset G as"
+  hence "fmset G bs \<le> fmset G as"
       by (rule divides_fmsubset) fact+
   with asubb
-      have "fmset G as = fmset G bs" by (simp add: mset_le_antisym)
+      have "fmset G as = fmset G bs" by (rule order_antisym)
   with anb
       show "False" ..
 qed
@@ -2354,7 +2354,7 @@
     and "wfactors G as a" and "wfactors G bs b"
     and "a \<in> carrier G" and "b \<in> carrier G"
     and "set as \<subseteq> carrier G" and "set bs \<subseteq> carrier G"
-  shows "fmset G as \<le># fmset G bs \<and> fmset G as \<noteq> fmset G bs"
+  shows "fmset G as \<le> fmset G bs \<and> fmset G as \<noteq> fmset G bs"
 using pf
 apply (elim properfactorE)
 apply rule
@@ -2738,12 +2738,12 @@
   have "c gcdof a b"
   proof (simp add: isgcd_def, safe)
     from csmset
-        have "fmset G cs \<le># fmset G as"
+        have "fmset G cs \<le> fmset G as"
         by (simp add: multiset_inter_def mset_le_def)
     thus "c divides a" by (rule fmsubset_divides) fact+
   next
     from csmset
-        have "fmset G cs \<le># fmset G bs"
+        have "fmset G cs \<le> fmset G bs"
         by (simp add: multiset_inter_def mset_le_def, force)
     thus "c divides b" by (rule fmsubset_divides) fact+
   next
@@ -2756,13 +2756,13 @@
         by auto
 
     assume "y divides a"
-    hence ya: "fmset G ys \<le># fmset G as" by (rule divides_fmsubset) fact+
+    hence ya: "fmset G ys \<le> fmset G as" by (rule divides_fmsubset) fact+
 
     assume "y divides b"
-    hence yb: "fmset G ys \<le># fmset G bs" by (rule divides_fmsubset) fact+
+    hence yb: "fmset G ys \<le> fmset G bs" by (rule divides_fmsubset) fact+
 
     from ya yb csmset
-    have "fmset G ys \<le># fmset G cs" by (simp add: mset_le_def multiset_inter_count)
+    have "fmset G ys \<le> fmset G cs" by (simp add: mset_le_def multiset_inter_count)
     thus "y divides c" by (rule fmsubset_divides) fact+
   qed
 
@@ -2837,10 +2837,10 @@
 
   have "c lcmof a b"
   proof (simp add: islcm_def, safe)
-    from csmset have "fmset G as \<le># fmset G cs" by (simp add: mset_le_def, force)
+    from csmset have "fmset G as \<le> fmset G cs" by (simp add: mset_le_def, force)
     thus "a divides c" by (rule fmsubset_divides) fact+
   next
-    from csmset have "fmset G bs \<le># fmset G cs" by (simp add: mset_le_def)
+    from csmset have "fmset G bs \<le> fmset G cs" by (simp add: mset_le_def)
     thus "b divides c" by (rule fmsubset_divides) fact+
   next
     fix y
@@ -2852,13 +2852,13 @@
         by auto
 
     assume "a divides y"
-    hence ya: "fmset G as \<le># fmset G ys" by (rule divides_fmsubset) fact+
+    hence ya: "fmset G as \<le> fmset G ys" by (rule divides_fmsubset) fact+
 
     assume "b divides y"
-    hence yb: "fmset G bs \<le># fmset G ys" by (rule divides_fmsubset) fact+
+    hence yb: "fmset G bs \<le> fmset G ys" by (rule divides_fmsubset) fact+
 
     from ya yb csmset
-    have "fmset G cs \<le># fmset G ys"
+    have "fmset G cs \<le> fmset G ys"
       apply (simp add: mset_le_def, clarify)
       apply (case_tac "count (fmset G as) a < count (fmset G bs) a")
        apply simp

--- a/src/HOL/Library/Permutation.thy	Mon Feb 22 09:15:10 2010 +0100
+++ b/src/HOL/Library/Permutation.thy	Mon Feb 22 09:15:10 2010 +0100
@@ -154,7 +154,7 @@
   done
 
 lemma multiset_of_le_perm_append:
-    "(multiset_of xs \<le># multiset_of ys) = (\<exists>zs. xs @ zs <~~> ys)"
+    "multiset_of xs \<le> multiset_of ys \<longleftrightarrow> (\<exists>zs. xs @ zs <~~> ys)"
   apply (auto simp: multiset_of_eq_perm[THEN sym] mset_le_exists_conv)
   apply (insert surj_multiset_of, drule surjD)
   apply (blast intro: sym)+