--- 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)
------------------------------
--- 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)