src/HOL/HOL.thy
changeset 13553 855f6bae851e
parent 13550 5a176b8dda84
child 13596 ee5f79b210c1
     1.1 --- a/src/HOL/HOL.thy	Sun Sep 01 19:39:25 2002 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Sep 02 11:07:26 2002 +0200
     1.3 @@ -651,7 +651,7 @@
     1.4    apply (rule order_refl)
     1.5    done
     1.6  
     1.7 -lemma order_less_irrefl [simp]: "~ x < (x::'a::order)"
     1.8 +lemma order_less_irrefl [iff]: "~ x < (x::'a::order)"
     1.9    by (simp add: order_less_le)
    1.10  
    1.11  lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"