src/HOL/Library/Multiset.thy
changeset 37765 26bdfb7b680b
parent 37751 89e16802b6cc
child 38242 f26d590dce0f
     1.1 --- a/src/HOL/Library/Multiset.thy	Mon Jul 12 08:58:12 2010 +0200
     1.2 +++ b/src/HOL/Library/Multiset.thy	Mon Jul 12 08:58:13 2010 +0200
     1.3 @@ -978,11 +978,11 @@
     1.4  subsubsection {* Well-foundedness *}
     1.5  
     1.6  definition mult1 :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
     1.7 -  [code del]: "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
     1.8 +  "mult1 r = {(N, M). \<exists>a M0 K. M = M0 + {#a#} \<and> N = M0 + K \<and>
     1.9        (\<forall>b. b :# K --> (b, a) \<in> r)}"
    1.10  
    1.11  definition mult :: "('a \<times> 'a) set => ('a multiset \<times> 'a multiset) set" where
    1.12 -  [code del]: "mult r = (mult1 r)\<^sup>+"
    1.13 +  "mult r = (mult1 r)\<^sup>+"
    1.14  
    1.15  lemma not_less_empty [iff]: "(M, {#}) \<notin> mult1 r"
    1.16  by (simp add: mult1_def)
    1.17 @@ -1498,7 +1498,7 @@
    1.18    by auto
    1.19  
    1.20  definition "ms_strict = mult pair_less"
    1.21 -definition [code del]: "ms_weak = ms_strict \<union> Id"
    1.22 +definition "ms_weak = ms_strict \<union> Id"
    1.23  
    1.24  lemma ms_reduction_pair: "reduction_pair (ms_strict, ms_weak)"
    1.25  unfolding reduction_pair_def ms_strict_def ms_weak_def pair_less_def