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/MicroJava/DFA/Kildall.thy
changeset 58860 fee7cfa69c50
parent 52847 820339715ffe
child 58886 8a6cac7c7247 
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -355,7 +355,7 @@
 apply(simp add: stables_def split_paired_all)
 apply(rename_tac ss w)
 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
- prefer 2; apply (fast intro: someI)
+ prefer 2 apply (fast intro: someI)
 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
  prefer 2
  apply clarify
@@ -406,7 +406,7 @@
 apply(simp add: stables_def split_paired_all)
 apply(rename_tac ss w)
 apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
- prefer 2; apply (fast intro: someI)
+ prefer 2 apply (fast intro: someI)
 apply(subgoal_tac "\<forall>(q,t) \<in> set (step (SOME p. p \<in> w) (ss ! (SOME p. p \<in> w))). q < length ss \<and> t \<in> A")
  prefer 2
  apply clarify
isabelle