src/HOL/Library/Multiset.thy
 changeset 27106 ff27dc6e7d05 parent 26818 b4a24433154e child 27368 9f90ac19e32b
```     1.1 --- a/src/HOL/Library/Multiset.thy	Tue Jun 10 15:30:54 2008 +0200
1.2 +++ b/src/HOL/Library/Multiset.thy	Tue Jun 10 15:30:56 2008 +0200
1.3 @@ -500,7 +500,7 @@
1.4
1.5  definition
1.6    mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
1.7 -  "mult1 r =
1.8 +  [code func del]:"mult1 r =
1.9      {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
1.10        (\<forall>b. b :# K --> (b, a) \<in> r)}"
1.11
1.12 @@ -716,10 +716,10 @@
1.13  begin
1.14
1.15  definition
1.16 -  less_multiset_def: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
1.17 +  less_multiset_def [code func del]: "M' < M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
1.18
1.19  definition
1.20 -  le_multiset_def: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
1.21 +  le_multiset_def [code func del]: "M' <= M \<longleftrightarrow> M' = M \<or> M' < (M::'a multiset)"
1.22
1.23  lemma trans_base_order: "trans {(x', x). x' < (x::'a::order)}"
1.24  unfolding trans_def by (blast intro: order_less_trans)
1.25 @@ -988,11 +988,11 @@
1.26
1.27  definition
1.28    mset_le :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<le>#" 50) where
1.29 -  "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
1.30 +  [code func del]: "(A \<le># B) = (\<forall>a. count A a \<le> count B a)"
1.31
1.32  definition
1.33    mset_less :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "<#" 50) where
1.34 -  "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
1.35 +  [code func del]: "(A <# B) = (A \<le># B \<and> A \<noteq> B)"
1.36
1.37  notation mset_le  (infix "\<subseteq>#" 50)
1.38  notation mset_less  (infix "\<subset>#" 50)
```