--- a/src/HOL/Analysis/Arcwise_Connected.thy Sun May 05 15:31:08 2024 +0100
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Mon May 06 14:39:33 2024 +0100
@@ -1103,13 +1103,15 @@
with Suc.prems show ?thesis by auto
next
case True
- show ?thesis proof (cases "even j")
+ show ?thesis
+ proof (cases "even j")
case True
then obtain k where k: "j = 2*k" by (metis evenE)
with \<open>0 < j\<close> have "k > 0" "2 * k < 2 ^ n"
using Suc.prems(2) k by auto
with k \<open>0 < n\<close> Suc.IH [of k] show ?thesis
- by (simp add: m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
+ apply (simp add: m1_to_3 a41 b43 del: power_Suc of_nat_diff)
+ by simp
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)
@@ -1145,7 +1147,7 @@
by auto
then show ?thesis
using Suc.IH [of k] k \<open>0 < k\<close>
- by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc) (auto simp: of_nat_diff)
+ by (simp add: less2n add.commute [of 1] m1_to_3 a41 b43 del: power_Suc of_nat_diff) auto
next
case False
then obtain k where k: "j = 2*k + 1" by (metis oddE)