diff -r 1aeafba76f21 -r 631dd866b284 src/HOL/IMP/Denotation.thy
--- a/src/HOL/IMP/Denotation.thy	Wed Jun 01 22:42:37 2011 +0200
+++ b/src/HOL/IMP/Denotation.thy	Wed Jun 01 22:47:26 2011 +0200
@@ -20,8 +20,6 @@
 "C(WHILE b DO c) = lfp (Gamma b (C c))"
 
 
-(**** mono (Gamma(b,c)) ****)
-
 lemma Gamma_mono: "mono (Gamma b c)"
 by (unfold Gamma_def mono_def) fast
 
@@ -31,10 +29,9 @@
 apply (simp add: Gamma_def)
 done
 
-(* Operational Semantics implies Denotational Semantics *)
+text{* Equivalence of denotational and big-step semantics: *}
 
 lemma com1: "(c,s) \<Rightarrow> t \<Longrightarrow> (s,t) \<in> C(c)"
-(* start with rule induction *)
 apply (induct rule: big_step_induct)
 apply auto
 (* while *)
@@ -45,8 +42,6 @@
 apply auto 
 done
 
-(* Denotational Semantics implies Operational Semantics *)
-
 lemma com2: "(s,t) \<in> C(c) \<Longrightarrow> (c,s) \<Rightarrow> t"
 apply (induct c arbitrary: s t)
 apply auto 
@@ -57,10 +52,7 @@
 apply auto
 done
 
-
-(**** Proof of Equivalence ****)
-
-lemma denotational_is_natural: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"
+lemma denotational_is_big_step: "(s,t) \<in> C(c)  =  ((c,s) \<Rightarrow> t)"
 by (fast elim: com2 dest: com1)
 
 end