src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Sun Sep 01 19:39:25 2002 +0200
+++ b/src/HOL/HOL.thy	Mon Sep 02 11:07:26 2002 +0200
@@ -651,7 +651,7 @@
   apply (rule order_refl)
   done
 
-lemma order_less_irrefl [simp]: "~ x < (x::'a::order)"
+lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
   by (simp add: order_less_le)
 
 lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"