src/HOL/Bali/AxSem.thy
changeset 24038 18182c4aec9e
parent 24019 67bde7cfcf10
child 24783 5a3e336a2e37
     1.1 --- a/src/HOL/Bali/AxSem.thy	Sun Jul 29 14:29:51 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Sun Jul 29 14:29:52 2007 +0200
     1.3 @@ -959,7 +959,7 @@
     1.4      G,(A::'a triple set)\<turnstile>{Normal (P C sig)::'a assn} mb C sig-\<succ> {Q C sig}\<rbrakk> \<Longrightarrow> 
     1.5         G,A|\<turnstile>{{P} mb-\<succ> {Q} | F}"
     1.6  apply (frule (1) finite_subset)
     1.7 -apply (erule make_imp)
     1.8 +apply (erule rev_mp)
     1.9  apply (erule thin_rl)
    1.10  apply (erule finite_induct)
    1.11  apply  (unfold mtriples_def)
    1.12 @@ -984,7 +984,7 @@
    1.13    ((\<forall>(C,sig)\<in>F. G,(A::'a triple set)\<turnstile>(f C sig::'a triple)) \<longrightarrow> (\<forall>(C,sig)\<in>ms. G,A\<turnstile>(g C sig::'a triple))) \<longrightarrow>  
    1.14        G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
    1.15  apply (frule (1) finite_subset)
    1.16 -apply (erule make_imp)
    1.17 +apply (erule rev_mp)
    1.18  apply (erule thin_rl)
    1.19  apply (erule finite_induct)
    1.20  apply  clarsimp+