
diff -r 493b818e8e10 -r fad29d2a17a5 src/HOL/Hull.thy
--- 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)
 




