tuned;
authorwenzelm
Wed Nov 21 00:32:10 2001 +0100 (2001-11-21)
changeset 1225626243ebf2831
parent 12255 93d4972238c7
child 12257 e3f7d6fb55d7
tuned;
src/HOL/HOL.thy
     1.1 --- a/src/HOL/HOL.thy	Tue Nov 20 22:54:06 2001 +0100
     1.2 +++ b/src/HOL/HOL.thy	Wed Nov 21 00:32:10 2001 +0100
     1.3 @@ -418,7 +418,7 @@
     1.4  lemma order_le_less: "((x::'a::order) <= y) = (x < y | x = y)"
     1.5      -- {* NOT suitable for iff, since it can cause PROOF FAILED. *}
     1.6    apply (simp add: order_less_le)
     1.7 -  apply (blast intro!: order_refl)
     1.8 +  apply blast
     1.9    done
    1.10  
    1.11  lemmas order_le_imp_less_or_eq = order_le_less [THEN iffD1, standard]