# HG changeset patch # User wenzelm # Date 1165761034 -3600 # Node ID f2be09171c9ccea9106bf820b29f182e79579141 # Parent ccb2346ee4167c681de2ecda67de9f6c424c0a81 hide const linorder.less_eq_less.max linorder.less_eq_less.min; diff -r ccb2346ee416 -r f2be09171c9c src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Sun Dec 10 15:30:33 2006 +0100 +++ b/src/HOL/Orderings.thy Sun Dec 10 15:30:34 2006 +0100 @@ -868,6 +868,8 @@ max :: "['a::ord, 'a] => 'a" "max a b == (if a <= b then b else a)" +hide const linorder.less_eq_less.max linorder.less_eq_less.min (* FIXME !? *) + lemma min_linorder: "linorder.min (op \ \ 'a\linorder \ 'a \ bool) = min" by (rule+) (simp add: min_def linorder.min_def)