# HG changeset patch
# User paulson
# Date 1183550186 -7200
# Node ID 42f2f90b51a645abf3ba3c9ee0426b8bc4313a7b
# Parent  6cad6b400cfd49e9f2c65d6c9839401b1515f042
simplified a proof

diff -r 6cad6b400cfd -r 42f2f90b51a6 src/HOL/Bali/AxSem.thy
--- a/src/HOL/Bali/AxSem.thy	Tue Jul 03 23:00:42 2007 +0200
+++ b/src/HOL/Bali/AxSem.thy	Wed Jul 04 13:56:26 2007 +0200
@@ -679,16 +679,9 @@
 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) 
 (* 37 subgoals *)
 prefer 18 (* Methd *)
-apply (rule ax_derivs.Methd, drule spec, erule mp, fast)
-apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
-                     THEN_ALL_NEW Blast_tac) *})
-apply (erule ax_derivs.Call)
-apply   clarify 
-apply   blast
-
-apply   (rule allI)+ 
-apply   (drule spec)+
-apply   blast
+apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
+apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *})
+apply auto
 done
 
 lemma ax_thin_insert: "G,(A::'a triple set)\<turnstile>(t::'a triple) \<Longrightarrow> G,insert x A\<turnstile>t"