tuned proofs;
authorwenzelm
Tue, 01 Sep 2020 16:57:54 +0200
changeset 72465 c17d0227205c
parent 72464 e5fcbf6dc687
child 72466 4d615ec4b6b1
tuned proofs;
src/HOL/Hoare_Parallel/Graph.thy
src/HOL/MicroJava/Comp/CorrCompTp.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)
--- 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