# HG changeset patch
# User wenzelm
# Date 1006299130 -3600
# Node ID 26243ebf2831d919c222db133cf26afba15e82ef
# Parent  93d4972238c709f0dbb284c90ece587b5d415fea
tuned;

diff -r 93d4972238c7 -r 26243ebf2831 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Nov 20 22:54:06 2001 +0100
+++ b/src/HOL/HOL.thy	Wed Nov 21 00:32:10 2001 +0100
@@ -418,7 +418,7 @@
 lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
     -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
   apply (simp add: order_less_le)
-  apply (blast intro!: order_refl)
+  apply blast
   done
 
 lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]