src/HOL/Orderings.thy
changeset 23032 b6cb6a131511
parent 23018 1d29bc31b0cb
child 23087 ad7244663431
     1.1 --- a/src/HOL/Orderings.thy	Sat May 19 13:41:13 2007 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Sat May 19 14:05:05 2007 +0200
     1.3 @@ -91,6 +91,9 @@
     1.4    max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
     1.5    "max a b = (if a \<le> b then b else a)"
     1.6  
     1.7 +declare min_def[code unfold, code inline del]
     1.8 +        max_def[code unfold, code inline del]
     1.9 +
    1.10  lemma linorder_class_min:
    1.11    "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
    1.12    by rule+ (simp add: min_def ord_class.min_def)