src/HOL/Bali/AxSem.thy
changeset 23894 1a4167d761ac
parent 23747 b07cff284683
child 24019 67bde7cfcf10
     1.1 --- a/src/HOL/Bali/AxSem.thy	Sat Jul 21 17:40:40 2007 +0200
     1.2 +++ b/src/HOL/Bali/AxSem.thy	Sat Jul 21 23:25:00 2007 +0200
     1.3 @@ -670,7 +670,7 @@
     1.4  lemma ax_thin [rule_format (no_asm)]: 
     1.5    "G,(A'::'a triple set)|\<turnstile>(ts::'a triple set) \<Longrightarrow> \<forall>A. A' \<subseteq> A \<longrightarrow> G,A|\<turnstile>ts"
     1.6  apply (erule ax_derivs.induct)
     1.7 -apply                (tactic "ALLGOALS(EVERY'[Clarify_tac,REPEAT o smp_tac 1])")
     1.8 +apply                (tactic "ALLGOALS(EVERY'[clarify_tac @{claset}, REPEAT o smp_tac 1])")
     1.9  apply                (rule ax_derivs.empty)
    1.10  apply               (erule (1) ax_derivs.insert)
    1.11  apply              (fast intro: ax_derivs.asm)
    1.12 @@ -712,7 +712,7 @@
    1.13  apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
    1.14  (*37 subgoals*)
    1.15  apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
    1.16 -                   THEN_ALL_NEW Fast_tac) *})
    1.17 +                   THEN_ALL_NEW fast_tac @{claset}) *})
    1.18  (*1 subgoal*)
    1.19  apply (clarsimp simp add: subset_mtriples_iff)
    1.20  apply (rule ax_derivs.Methd)