src/HOL/Bali/AxSem.thy
changeset 61424 c3658c18b7bc
parent 60754 02924903a6fd
child 61989 ba8c284d4725
     1.1 --- a/src/HOL/Bali/AxSem.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -969,7 +969,7 @@
     1.4  done
     1.5  
     1.6  lemma ax_methods_spec: 
     1.7 -"\<lbrakk>G,(A::'a triple set)|\<turnstile>split f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
     1.8 +"\<lbrakk>G,(A::'a triple set)|\<turnstile>case_prod f ` ms; (C,sig) \<in> ms\<rbrakk>\<Longrightarrow> G,A\<turnstile>((f C sig)::'a triple)"
     1.9  apply (erule ax_derivs.weaken)
    1.10  apply (force del: image_eqI intro: rev_image_eqI)
    1.11  done
    1.12 @@ -977,7 +977,7 @@
    1.13  (* this version is used to avoid using the cut rule *)
    1.14  lemma ax_finite_pointwise_lemma [rule_format]: "\<lbrakk>F \<subseteq> ms; finite ms\<rbrakk> \<Longrightarrow>  
    1.15    ((\<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.16 -      G,A|\<turnstile>split f ` F \<longrightarrow> G,A|\<turnstile>split g ` F"
    1.17 +      G,A|\<turnstile>case_prod f ` F \<longrightarrow> G,A|\<turnstile>case_prod g ` F"
    1.18  apply (frule (1) finite_subset)
    1.19  apply (erule rev_mp)
    1.20  apply (erule thin_rl)