diff -r 403d4e0ad712 -r e21b2f888fa2 CookBook/Package/Ind_Examples.thy
--- a/CookBook/Package/Ind_Examples.thy	Mon Oct 13 17:53:13 2008 +0200
+++ b/CookBook/Package/Ind_Examples.thy	Tue Oct 14 01:33:55 2008 -0400
@@ -160,7 +160,8 @@
 
 lemma even_induct:
   assumes even: "even n"
-  shows "P 0 \<Longrightarrow> (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+  shows "P 0 \<Longrightarrow> 
+             (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
   apply (atomize (full))
   apply (cut_tac even)
   apply (unfold even_def)