removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
authorbulwahn
Mon, 24 Oct 2011 12:26:05 +0200
changeset 45261 8716790fe5a3
parent 45260 48295059cef3
child 45262 b0cea4362430
removing poor man's dictionary construction which were only for the ancient code generator with no support of type classes
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 *}