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 67613 ce654b0e6d69
parent 67443 3abf6a722518
child 68249 949d93804740 
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -203,7 +203,7 @@
      q \<notin> w \<or> q = p \<rbrakk> 
   \<Longrightarrow> stable r step (merges f (step p (ss!p)) ss) q"
   apply (unfold stable_def)
-  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' : A")
+  apply (subgoal_tac "\<forall>s'. (q,s') \<in> set (step p (ss!p)) \<longrightarrow> s' \<in> A")
    prefer 2
    apply clarify
    apply (erule pres_typeD)
isabelle