author | nipkow |
Mon, 02 Sep 2002 11:07:26 +0200 | |
changeset 13553 | 855f6bae851e |
parent 13552 | 83d674e8cd2a |
child 13554 | 4679359bb218 |
src/HOL/HOL.thy | file | annotate | diff | comparison | revisions |
--- 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)"