# HG changeset patch
# User haftmann
# Date 1223388441 -7200
# Node ID e6fdcaaadbd35bdc366fcbef5439f800db5d79d5
# Parent  b26ba1b1dbda881585a7223a6b94f59aac1964ee
tuned min/max code generation

diff -r b26ba1b1dbda -r e6fdcaaadbd3 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Tue Oct 07 16:07:20 2008 +0200
+++ b/src/HOL/Orderings.thy	Tue Oct 07 16:07:21 2008 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Orderings.thy
+ (*  Title:      HOL/Orderings.thy
     ID:         $Id$
     Author:     Tobias Nipkow, Markus Wenzel, and Larry Paulson
 *)
@@ -7,8 +7,7 @@
 
 theory Orderings
 imports Code_Setup
-uses
-  "~~/src/Provers/order.ML"
+uses "~~/src/Provers/order.ML"
 begin
 
 subsection {* Quasi orders *}
@@ -229,10 +228,10 @@
 text {* min/max *}
 
 definition (in ord) min :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  [code unfold, code inline del]: "min a b = (if a \<le> b then a else b)"
+  [code del]: "min a b = (if a \<le> b then a else b)"
 
 definition (in ord) max :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
-  [code unfold, code inline del]: "max a b = (if a \<le> b then b else a)"
+  [code del]: "max a b = (if a \<le> b then b else a)"
 
 lemma min_le_iff_disj:
   "min x y \<le> z \<longleftrightarrow> x \<le> z \<or> y \<le> z"
@@ -268,6 +267,20 @@
 
 end
 
+text {* Explicit dictionaries for code generation *}
+
+lemma min_ord_min [code, code unfold, code inline del]:
+  "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, code unfold, code inline del]:
+  "max = ord.max (op \<le>)"
+  by (rule ext)+ (simp add: max_def ord.max_def)
+
+declare ord.max_def [code]
+
 
 subsection {* Reasoning tools setup *}