added lemma

--- a/src/HOL/IMP/Denotational.thy	Thu Jun 20 17:26:16 2013 +0200
+++ b/src/HOL/IMP/Denotational.thy	Thu Jun 20 17:43:36 2013 +0200
@@ -59,6 +59,9 @@
   "(s,t) \<in> D(c)  =  ((c,s) \<Rightarrow> t)"
 by (metis D_if_big_step Big_step_if_D[simplified])
 
+corollary equiv_c_iff_equal_D: "(c1 \<sim> c2) \<longleftrightarrow> D c1 = D c2"
+by(simp add: denotational_is_big_step[symmetric] set_eq_iff)
+
 
 subsection "Continuity"