simplified a proof
authorpaulson
Wed Jul 04 13:56:26 2007 +0200 (2007-07-04)
changeset 2356342f2f90b51a6
parent 23562 6cad6b400cfd
child 23564 ae0e735fbec8
simplified a proof
src/HOL/Bali/AxSem.thy
     1.1 --- a/src/HOL/Bali/AxSem.thy	Tue Jul 03 23:00:42 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Wed Jul 04 13:56:26 2007 +0200
     1.3 @@ -679,16 +679,9 @@
     1.4  apply           (rule ax_derivs.conseq, intro strip, tactic "smp_tac 3 1",clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) 
     1.5  (* 37 subgoals *)
     1.6  prefer 18 (* Methd *)
     1.7 -apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
     1.8 -apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
     1.9 -                     THEN_ALL_NEW Blast_tac) *})
    1.10 -apply (erule ax_derivs.Call)
    1.11 -apply   clarify 
    1.12 -apply   blast
    1.13 -
    1.14 -apply   (rule allI)+ 
    1.15 -apply   (drule spec)+
    1.16 -apply   blast
    1.17 +apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
    1.18 +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *})
    1.19 +apply auto
    1.20  done
    1.21  
    1.22  lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"