diff -r 75f488e15479 -r 37a74da77be7 src/HOL/Eisbach/Examples.thy
--- 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