--- a/src/HOL/HOL.thy Fri Sep 27 16:44:50 2002 +0200
+++ b/src/HOL/HOL.thy Mon Sep 30 15:44:21 2002 +0200
@@ -857,8 +857,6 @@
apply (blast intro: order_less_trans)
done
-declare order_less_irrefl [iff]
-
lemma max_assoc: "!!x::'a::linorder. max (max x y) z = max x (max y z)"
apply(simp add:max_def)
apply(rule conjI)
@@ -897,9 +895,6 @@
lemmas min_ac = min_assoc min_commute
mk_left_commute[of min,OF min_assoc min_commute]
-declare order_less_irrefl [iff del]
-declare order_less_irrefl [simp]
-
lemma split_min:
"P (min (i::'a::linorder) j) = ((i <= j --> P(i)) & (~ i <= j --> P(j)))"
by (simp add: min_def)