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)