# 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 \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min"
   by (rule+) (simp add: min_def linorder.min_def)