# HG changeset patch
# User bulwahn
# Date 1319451965 -7200
# Node ID 8716790fe5a30847d7356cc50ee8c7076f4fae2f
# Parent  48295059cef303ac7f49c053a2fdb72d43f3ddf1
removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes

diff -r 48295059cef3 -r 8716790fe5a3 src/HOL/Orderings.thy
--- 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 *}