diff -r 7e6cdcd113a2 -r ee5f79b210c1 src/HOL/HOL.thy
--- 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)