src/HOL/MicroJava/DFA/Kildall.thy
changeset 58860 fee7cfa69c50
parent 52847 820339715ffe
child 58886 8a6cac7c7247
     1.1 --- a/src/HOL/MicroJava/DFA/Kildall.thy	Sat Nov 01 11:40:55 2014 +0100
     1.2 +++ b/src/HOL/MicroJava/DFA/Kildall.thy	Sat Nov 01 14:20:38 2014 +0100
     1.3 @@ -355,7 +355,7 @@
     1.4  apply(simp add: stables_def split_paired_all)
     1.5  apply(rename_tac ss w)
     1.6  apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
     1.7 - prefer 2; apply (fast intro: someI)
     1.8 + prefer 2 apply (fast intro: someI)
     1.9  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")
    1.10   prefer 2
    1.11   apply clarify
    1.12 @@ -406,7 +406,7 @@
    1.13  apply(simp add: stables_def split_paired_all)
    1.14  apply(rename_tac ss w)
    1.15  apply(subgoal_tac "(SOME p. p \<in> w) \<in> w")
    1.16 - prefer 2; apply (fast intro: someI)
    1.17 + prefer 2 apply (fast intro: someI)
    1.18  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")
    1.19   prefer 2
    1.20   apply clarify