--- a/src/HOL/Inductive.thy Sat Oct 01 17:38:14 2016 +0200
+++ b/src/HOL/Inductive.thy Sat Oct 01 19:29:48 2016 +0200
@@ -23,10 +23,10 @@
where "lfp f = Inf {u. f u \<le> u}"
lemma lfp_lowerbound: "f A \<le> A \<Longrightarrow> lfp f \<le> A"
- by (auto simp add: lfp_def intro: Inf_lower)
+ unfolding lfp_def by (rule Inf_lower) simp
lemma lfp_greatest: "(\<And>u. f u \<le> u \<Longrightarrow> A \<le> u) \<Longrightarrow> A \<le> lfp f"
- by (auto simp add: lfp_def intro: Inf_greatest)
+ unfolding lfp_def by (rule Inf_greatest) simp
end