--- a/src/HOL/Library/Discrete.thy Fri Jul 22 08:02:37 2016 +0200
+++ b/src/HOL/Library/Discrete.thy Fri Jul 22 11:00:43 2016 +0200
@@ -28,11 +28,13 @@
assume "n > 0"
show "P n"
proof (cases "n = 1")
- case True with one show ?thesis by simp
+ case True
+ with one show ?thesis by simp
next
- case False with \<open>n > 0\<close> have "n \<ge> 2" by auto
- moreover with * have "P (n div 2)" .
- ultimately show ?thesis by (rule double)
+ case False
+ with \<open>n > 0\<close> have "n \<ge> 2" by auto
+ with * have "P (n div 2)" .
+ with \<open>n \<ge> 2\<close> show ?thesis by (rule double)
qed
qed