--- a/src/HOL/Orderings.thy Mon Oct 24 11:40:31 2011 +0200
+++ b/src/HOL/Orderings.thy Mon Oct 24 12:26:05 2011 +0200
@@ -303,20 +303,6 @@
end
-text {* Explicit dictionaries for code generation *}
-
-lemma min_ord_min [code]:
- "min = ord.min (op \<le>)"
- by (rule ext)+ (simp add: min_def ord.min_def)
-
-declare ord.min_def [code]
-
-lemma max_ord_max [code]:
- "max = ord.max (op \<le>)"
- by (rule ext)+ (simp add: max_def ord.max_def)
-
-declare ord.max_def [code]
-
subsection {* Reasoning tools setup *}