# HG changeset patch
# User fleury <Mathias.Fleury@mpi-inf.mpg.de>
# Date 1433944217 -7200
# Node ID a8a31b9ebff596c0f324361482ff6b6a61d723b2
# Parent  b3f54cde0216d33a788637de85b615394ca5931e
tuned

diff -r b3f54cde0216 -r a8a31b9ebff5 NEWS
--- a/NEWS	Wed Jun 10 13:44:46 2015 +0200
+++ b/NEWS	Wed Jun 10 15:50:17 2015 +0200
@@ -65,7 +65,12 @@
   - Renamed lemmas:
       mset_le_def ~> subseteq_mset_def
       mset_less_def ~> subset_mset_def
-
+      less_eq_multiset.rep_eq ~> subseteq_mset_def
+    INCOMPATIBILITY
+  - Removed lemmas generated by lift_definition:
+    less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer
+    less_eq_multiset_def
+    INCOMPATIBILITY
 
 New in Isabelle2015 (May 2015)
 ------------------------------
diff -r b3f54cde0216 -r a8a31b9ebff5 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Jun 10 13:44:46 2015 +0200
+++ b/src/HOL/Library/Multiset.thy	Wed Jun 10 15:50:17 2015 +0200
@@ -281,10 +281,10 @@
 subsubsection {* Pointwise ordering induced by count *}
 
 definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
-"subseteq_mset A B \<equiv> (\<forall>a. count A a \<le> count B a)"
+"subseteq_mset A B = (\<forall>a. count A a \<le> count B a)"
 
 definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
-"subset_mset A B \<equiv> (A <=# B \<and> A \<noteq> B)"
+"subset_mset A B = (A <=# B \<and> A \<noteq> B)"
 
 notation subseteq_mset (infix "\<le>#" 50)
 notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)