src/HOL/IMP/Denotation.thy
changeset 15481 fc075ae929e4
parent 12434 ff2efde4574d
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/IMP/Denotation.thy	Sun Jan 30 20:48:50 2005 +0100
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Tue Feb 01 18:01:57 2005 +0100
     1.3 @@ -34,15 +34,13 @@
     1.4  
     1.5  lemma C_While_If: "C(\<WHILE> b \<DO> c) = C(\<IF> b \<THEN> c;\<WHILE> b \<DO> c \<ELSE> \<SKIP>)"
     1.6  apply (simp (no_asm)) 
     1.7 -apply (subst lfp_unfold [OF Gamma_mono]) back back
     1.8 -apply (subst Gamma_def [THEN meta_eq_to_obj_eq, THEN fun_cong]) 
     1.9 -apply simp
    1.10 +apply (subst lfp_unfold [OF Gamma_mono])  --{*lhs only*}
    1.11 +apply (simp add: Gamma_def)
    1.12  done
    1.13  
    1.14  (* Operational Semantics implies Denotational Semantics *)
    1.15  
    1.16  lemma com1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t \<Longrightarrow> (s,t) \<in> C(c)"
    1.17 -
    1.18  (* start with rule induction *)
    1.19  apply (erule evalc.induct)
    1.20  apply auto