src/HOL/Bali/AxSem.thy
changeset 39159 0dec18004e75
parent 37956 ee939247b2fb
child 41778 5f79a9e42507
     1.1 --- a/src/HOL/Bali/AxSem.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -671,7 +671,7 @@
     1.4  (* 37 subgoals *)
     1.5  prefer 18 (* Methd *)
     1.6  apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
     1.7 -apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *})
     1.8 +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})) *})
     1.9  apply auto
    1.10  done
    1.11  
    1.12 @@ -691,8 +691,8 @@
    1.13  apply (erule ax_derivs.induct)
    1.14  (*42 subgoals*)
    1.15  apply       (tactic "ALLGOALS strip_tac")
    1.16 -apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
    1.17 -         etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
    1.18 +apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
    1.19 +         etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*})
    1.20  apply       (tactic "TRYALL hyp_subst_tac")
    1.21  apply       (simp, rule ax_derivs.empty)
    1.22  apply      (drule subset_insertD)
    1.23 @@ -702,7 +702,7 @@
    1.24  apply   (fast intro: ax_derivs.weaken)
    1.25  apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
    1.26  (*37 subgoals*)
    1.27 -apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
    1.28 +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros}) 
    1.29                     THEN_ALL_NEW fast_tac @{claset}) *})
    1.30  (*1 subgoal*)
    1.31  apply (clarsimp simp add: subset_mtriples_iff)