src/HOL/IMP/Denotational.thy

--- a/src/HOL/IMP/Denotational.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/IMP/Denotational.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -44,7 +44,7 @@
 abbreviation Big_step :: "com \<Rightarrow> com_den" where
 "Big_step c \<equiv> {(s,t). (c,s) \<Rightarrow> t}"
 
-lemma Big_step_if_D:  "(s,t) \<in> D(c) \<Longrightarrow> (s,t) : Big_step c"
+lemma Big_step_if_D:  "(s,t) \<in> D(c) \<Longrightarrow> (s,t) \<in> Big_step c"
 proof (induction c arbitrary: s t)
   case Seq thus ?case by fastforce
 next