src/HOL/Orderings.thy
changeset 45261 8716790fe5a3
parent 45231 d85a2fdc586c
child 45262 b0cea4362430
     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