--- a/src/HOL/Eisbach/Examples.thy Mon Apr 18 14:47:27 2016 +0200
+++ b/src/HOL/Eisbach/Examples.thy Mon Apr 18 15:13:46 2016 +0200
@@ -183,7 +183,7 @@
apply prop_solver
done
-lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P z \<Longrightarrow> P y \<Longrightarrow> Q y"
+lemma "(\<forall>x. P x \<longrightarrow> Q x) \<Longrightarrow> P z \<Longrightarrow> P y \<Longrightarrow> Q y"
apply (solves \<open>guess_all, prop_solver\<close>) \<comment> \<open>Try it without solve\<close>
done