Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Hoare_Parallel/Graph.thy
changeset 72233 c17d0227205c
parent 67443 3abf6a722518 
--- 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)
isabelle