order_less_irrefl: [simp] -> [iff]
authornipkow
Mon, 02 Sep 2002 11:07:26 +0200
changeset 13553 855f6bae851e
parent 13552 83d674e8cd2a
child 13554 4679359bb218
order_less_irrefl: [simp] -> [iff]
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)"