src/HOL/Orderings.thy

 
 lemma less_irrefl [iff]: "\<not> x < x"
 by (simp add: less_le_not_le)
 
 lemma less_imp_le: "x < y \<Longrightarrow> x \<le> y"
-unfolding less_le_not_le by blast
+by (simp add: less_le_not_le)
 
 
 text \<open>Asymmetry.\<close>
 
 lemma less_not_sym: "x < y \<Longrightarrow> \<not> (y < x)"

 lemma le_less: "x \<le> y \<longleftrightarrow> x < y \<or> x = y"
     \<comment> \<open>NOT suitable for iff, since it can cause PROOF FAILED.\<close>
 by (fact order.order_iff_strict)
 
 lemma le_imp_less_or_eq: "x \<le> y \<Longrightarrow> x < y \<or> x = y"
-unfolding less_le by blast
+by (simp add: less_le)
 
 
 text \<open>Useful for simplification, but too risky to include by default.\<close>
 
 lemma less_imp_not_eq: "x < y \<Longrightarrow> (x = y) \<longleftrightarrow> False"