fix for previous commit

Wed, 12 Jun 2019 18:52:53 +0200

author
Julian Brunner <julianbrunner@gmail.com>
date
Wed, 12 Jun 2019 18:52:53 +0200
changeset 10463
cf0914a2304e
parent 10462
6197fe173c6f
child 10464
f6b91be1ab2d

fix for previous commit

thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Translate.thy file | annotate | diff | comparison | revisions
--- a/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Translate.thy	Wed Jun 12 18:37:40 2019 +0200
+++ b/thys/Transition_Systems_and_Automata/Automata/NBA/NBA_Translate.thy	Wed Jun 12 18:52:53 2019 +0200
@@ -66,7 +66,7 @@
       (\<Union> p \<in> insert x T. \<Union> a \<in> alphabet A. f ` {p} \<times> {a} \<times> f ` transition A a p)" by auto
     fix Ta xa
     assume 2: "Ta \<subseteq> alphabet A" "xa \<in> alphabet A" "xa \<notin> Ta"
-    show "finite (transition A xa x)" using 1 2 assms(1) by (meson infinite_subset nodes_succ subsetI)
+    show "finite (transition A xa x)" using 1 2 assms(1) by (meson infinite_subset nodes_step subsetI)
     show "(f ` {x} \<times> {xa} \<times> f ` transition A xa x) \<union>
       (\<Union> a \<in> Ta. f ` {x} \<times> {a} \<times> f ` transition A a x) \<union>
       (\<Union> p \<in> T. \<Union> a \<in> alphabet A. f ` {p} \<times> {a} \<times> f ` transition A a p) =

mercurial