1.1 --- a/src/HOL/Orderings.thy	Mon Oct 24 11:40:31 2011 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Mon Oct 24 12:26:05 2011 +0200
     1.3 @@ -303,20 +303,6 @@
     1.4  
     1.5  end
     1.6  
     1.7 -text {* Explicit dictionaries for code generation *}
     1.8 -
     1.9 -lemma min_ord_min [code]:
    1.10 -  "min = ord.min (op \<le>)"
    1.11 -  by (rule ext)+ (simp add: min_def ord.min_def)
    1.12 -
    1.13 -declare ord.min_def [code]
    1.14 -
    1.15 -lemma max_ord_max [code]:
    1.16 -  "max = ord.max (op \<le>)"
    1.17 -  by (rule ext)+ (simp add: max_def ord.max_def)
    1.18 -
    1.19 -declare ord.max_def [code]
    1.20 -
    1.21  
    1.22  subsection {* Reasoning tools setup *}
    1.23