Commit 37bcb2de by benkeks

isabelle 2018 cont

parent 037e2b91
......@@ -39,7 +39,7 @@ shows
"q \<longmapsto> a q' \<Longrightarrow> (\<exists> p'. R p' q' \<and> (p \<longmapsto> a p'))"
using assms unfolding bisimulation_def by auto
end --"context lts"
end \<comment>\<open>context lts\<close>
end
\ No newline at end of file
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment