src/HOL/IMP/Transition.thy
changeset 12566 fe20540bcf93
parent 12546 0c90e581379f
child 13524 604d0f3622d6
     1.1 --- a/src/HOL/IMP/Transition.thy	Thu Dec 20 17:08:55 2001 +0100
     1.2 +++ b/src/HOL/IMP/Transition.thy	Thu Dec 20 18:22:44 2001 +0100
     1.3 @@ -501,12 +501,12 @@
     1.4  apply (fast dest: rtrancl_imp_UN_rel_pow intro: semiI)
     1.5  
     1.6  -- IF 
     1.7 -apply (fast intro: rtrancl_into_rtrancl2)
     1.8 -apply (fast intro: rtrancl_into_rtrancl2)
     1.9 +apply (fast intro: converse_rtrancl_into_rtrancl)
    1.10 +apply (fast intro: converse_rtrancl_into_rtrancl)
    1.11  
    1.12  -- WHILE 
    1.13  apply fast
    1.14 -apply (fast dest: rtrancl_imp_UN_rel_pow intro: rtrancl_into_rtrancl2 semiI)
    1.15 +apply (fast dest: rtrancl_imp_UN_rel_pow intro: converse_rtrancl_into_rtrancl semiI)
    1.16  
    1.17  done
    1.18  
    1.19 @@ -518,7 +518,7 @@
    1.20   apply fastsimp
    1.21  -- "induction step"
    1.22  apply (fast intro!: le_SucI le_refl dest!: rel_pow_Suc_D2 
    1.23 -            elim!: rel_pow_imp_rtrancl rtrancl_into_rtrancl2)
    1.24 +            elim!: rel_pow_imp_rtrancl converse_rtrancl_into_rtrancl)
    1.25  done
    1.26  
    1.27  lemma evalc1_impl_evalc [rule_format (no_asm)]: 
    1.28 @@ -598,7 +598,7 @@
    1.29       apply fast 
    1.30      apply clarify
    1.31      apply (case_tac c)
    1.32 -    apply (auto intro: rtrancl_into_rtrancl2)
    1.33 +    apply (auto intro: converse_rtrancl_into_rtrancl)
    1.34      done
    1.35    moreover assume "\<langle>c1,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* \<langle>s2\<rangle>" "\<langle>c2,s2\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3"
    1.36    ultimately show "\<langle>c1;c2,s1\<rangle> \<longrightarrow>\<^sub>1\<^sup>* cs3" by simp
    1.37 @@ -617,12 +617,12 @@
    1.38  apply (fast intro: my_lemma1)
    1.39  
    1.40  -- IF
    1.41 -apply (fast intro: rtrancl_into_rtrancl2)
    1.42 -apply (fast intro: rtrancl_into_rtrancl2) 
    1.43 +apply (fast intro: converse_rtrancl_into_rtrancl)
    1.44 +apply (fast intro: converse_rtrancl_into_rtrancl) 
    1.45  
    1.46  -- WHILE 
    1.47  apply fast
    1.48 -apply (fast intro: rtrancl_into_rtrancl2 my_lemma1)
    1.49 +apply (fast intro: converse_rtrancl_into_rtrancl my_lemma1)
    1.50  
    1.51  done
    1.52