# HG changeset patch
# User nipkow
# Date 1371743016 -7200
# Node ID 56e83c57f95391ae0032e35d9546f7cb7df64979
# Parent  ded7b9c60dc272770edeb15ddd91fb5b64c77dda
added lemma

diff -r ded7b9c60dc2 -r 56e83c57f953 src/HOL/IMP/Denotational.thy
--- 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"