# HG changeset patch
# User nipkow
# Date 1179576305 -7200
# Node ID b6cb6a1315114b1e4ab1991975dfee585f47ad19
# Parent  9da9585c816e13b9282e8e9b779e5aa0c9248b29
unfold min/max in Stefans code generator

diff -r 9da9585c816e -r b6cb6a131511 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sat May 19 13:41:13 2007 +0200
+++ b/src/HOL/Orderings.thy	Sat May 19 14:05:05 2007 +0200
@@ -91,6 +91,9 @@
   max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
   "max a b = (if a \<le> b then b else a)"
 
+declare min_def[code unfold, code inline del]
+        max_def[code unfold, code inline del]
+
 lemma linorder_class_min:
   "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
   by rule+ (simp add: min_def ord_class.min_def)