--- a/src/HOL/Hull.thy Wed May 02 13:49:38 2018 +0200
+++ b/src/HOL/Hull.thy Thu May 03 15:07:14 2018 +0200
@@ -47,7 +47,7 @@
lemma hull_unique: "s \<subseteq> t \<Longrightarrow> S t \<Longrightarrow> (\<And>t'. s \<subseteq> t' \<Longrightarrow> S t' \<Longrightarrow> t \<subseteq> t') \<Longrightarrow> (S hull s = t)"
unfolding hull_def by auto
-lemma hull_induct: "(\<And>x. x\<in> S \<Longrightarrow> P x) \<Longrightarrow> Q {x. P x} \<Longrightarrow> \<forall>x\<in> Q hull S. P x"
+lemma hull_induct: "\<lbrakk>a \<in> Q hull S; \<And>x. x\<in> S \<Longrightarrow> P x; Q {x. P x}\<rbrakk> \<Longrightarrow> P a"
using hull_minimal[of S "{x. P x}" Q]
by (auto simp add: subset_eq)