# 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 \)" - by (rule ext)+ (simp add: min_def ord.min_def) - -declare ord.min_def [code] - -lemma max_ord_max [code]: - "max = ord.max (op \)" - by (rule ext)+ (simp add: max_def ord.max_def) - -declare ord.max_def [code] - subsection {* Reasoning tools setup *}