src/HOL/IMP/Transition.thy
changeset 13524 604d0f3622d6
parent 12566 fe20540bcf93
child 14565 c6dc17aab88a
     1.1 --- a/src/HOL/IMP/Transition.thy	Tue Aug 27 11:03:02 2002 +0200
     1.2 +++ b/src/HOL/IMP/Transition.thy	Tue Aug 27 11:03:05 2002 +0200
     1.3 @@ -604,7 +604,7 @@
     1.4    ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
     1.5  qed
     1.6  
     1.7 -lemma evalc_impl_evalc1: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
     1.8 +lemma evalc_impl_evalc1': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>c s1 \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s1\<rangle>"
     1.9  apply (erule evalc.induct)
    1.10  
    1.11  -- SKIP 
    1.12 @@ -680,7 +680,7 @@
    1.13    apply (fastsimp elim!: evalc1_term_cases intro: FB_lemma3)
    1.14    done
    1.15  
    1.16 -lemma evalc1_impl_evalc: "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    1.17 +lemma evalc1_impl_evalc': "\<langle>c,s\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>t\<rangle> \<Longrightarrow> \<langle>c,s\<rangle> \<longrightarrow>\<^sub>c t"
    1.18    apply (fastsimp dest: FB_lemma2)
    1.19    done
    1.20