src/HOL/Library/Multiset.thy
changeset 59986 f38b94549dc8
parent 59958 4538d41e8e54
child 59997 90fb391a15c1
child 59998 c54d36be22ef
     1.1 --- a/src/HOL/Library/Multiset.thy	Thu Apr 09 15:54:09 2015 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Thu Apr 09 18:00:58 2015 +0200
     1.3 @@ -295,6 +295,18 @@
     1.4  
     1.5  end
     1.6  
     1.7 +abbreviation less_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
     1.8 +  "A <# B \<equiv> A < B"
     1.9 +abbreviation (xsymbols) subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50) where
    1.10 +  "A \<subset># B \<equiv> A < B"
    1.11 +
    1.12 +abbreviation less_eq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
    1.13 +  "A <=# B \<equiv> A \<le> B"
    1.14 +abbreviation (xsymbols) leq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<le>#" 50) where
    1.15 +  "A \<le># B \<equiv> A \<le> B"
    1.16 +abbreviation (xsymbols) subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subseteq>#" 50) where
    1.17 +  "A \<subseteq># B \<equiv> A \<le> B"
    1.18 +
    1.19  lemma mset_less_eqI:
    1.20    "(\<And>x. count A x \<le> count B x) \<Longrightarrow> A \<le> B"
    1.21    by (simp add: mset_le_def)