order_less_irrefl: [simp] -> [iff]
authornipkow
Mon Sep 02 11:07:26 2002 +0200 (2002-09-02)
changeset 13553855f6bae851e
parent 13552 83d674e8cd2a
child 13554 4679359bb218
order_less_irrefl: [simp] -> [iff]
src/HOL/HOL.thy
     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)"