# HG changeset patch
# User nipkow
# Date 1030957646 -7200
# Node ID 855f6bae851edfe8cad0be5e413615844fa1347c
# Parent  83d674e8cd2a63c5b1d0ac1b9c98f75a1b4829f8
order_less_irrefl: [simp] -> [iff]

diff -r 83d674e8cd2a -r 855f6bae851e 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)"