--- 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)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Mon Aug 31 22:05:05 2020 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Tue Sep 01 16:57:54 2020 +0200
@@ -451,10 +451,7 @@
"max_of_list (xs @ ys) = max (max_of_list xs) (max_of_list ys)"
apply (simp add: max_of_list_def)
apply (induct xs)
- apply simp
- using [[linarith_split_limit = 0]]
- apply simp
- apply arith
+ apply simp_all
done