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)
```