diff -r e5fcbf6dc687 -r c17d0227205c src/HOL/Hoare_Parallel/Graph.thy
--- a/src/HOL/Hoare_Parallel/Graph.thy	Mon Aug 31 22:05:05 2020 +0200
+++ b/src/HOL/Hoare_Parallel/Graph.thy	Tue Sep 01 16:57:54 2020 +0200
@@ -168,9 +168,7 @@
  prefer 2 apply arith
  apply(drule_tac n = "Suc nata" in Compl_lemma)
  apply clarify
- using [[linarith_split_limit = 0]]
- apply force
- using [[linarith_split_limit = 9]]
+ subgoal using [[linarith_split_limit = 0]] by force
 apply(drule leI)
 apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
  apply(erule_tac x = "m - (Suc nata)" in allE)