src/HOL/Bali/AxSound.thy
changeset 58963 26bf09b95dda
parent 58887 38db8ddc0f57
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/AxSound.thy	Sun Nov 09 20:49:28 2014 +0100
     1.2 +++ b/src/HOL/Bali/AxSound.thy	Mon Nov 10 21:49:48 2014 +0100
     1.3 @@ -50,13 +50,13 @@
     1.4  apply (rule iffI)
     1.5  apply  fast
     1.6  apply clarify
     1.7 -apply (tactic "smp_tac 3 1")
     1.8 +apply (tactic "smp_tac @{context} 3 1")
     1.9  apply (case_tac "normal s")
    1.10  apply  clarsimp
    1.11  apply  (elim conjE impE)
    1.12  apply    blast
    1.13  
    1.14 -apply    (tactic "smp_tac 2 1")
    1.15 +apply    (tactic "smp_tac @{context} 2 1")
    1.16  apply    (drule evaln_eval)
    1.17  apply    (drule (1) eval_type_sound [THEN conjunct1],simp, assumption+)
    1.18  apply    simp
    1.19 @@ -84,7 +84,7 @@
    1.20  "\<lbrakk>G\<Turnstile>n\<Colon>{Normal P} body G C sig-\<succ>{Q}\<rbrakk> 
    1.21    \<Longrightarrow> G\<Turnstile>Suc n\<Colon>{Normal P} Methd C sig-\<succ> {Q}"
    1.22  apply (simp (no_asm_use) add: triple_valid2_def2)
    1.23 -apply (intro strip, tactic "smp_tac 3 1", clarify)
    1.24 +apply (intro strip, tactic "smp_tac @{context} 3 1", clarify)
    1.25  apply (erule wt_elim_cases, erule da_elim_cases, erule evaln_elim_cases)
    1.26  apply (unfold body_def Let_def)
    1.27  apply (clarsimp simp add: inj_term_simps)
    1.28 @@ -400,14 +400,14 @@
    1.29        from valid_A conf wt da eval P con
    1.30        have "Q v s1 Z"
    1.31          apply (simp add: ax_valids2_def triple_valid2_def2)
    1.32 -        apply (tactic "smp_tac 3 1")
    1.33 +        apply (tactic "smp_tac @{context} 3 1")
    1.34          apply clarify
    1.35 -        apply (tactic "smp_tac 1 1")
    1.36 +        apply (tactic "smp_tac @{context} 1 1")
    1.37          apply (erule allE,erule allE, erule mp)
    1.38          apply (intro strip)
    1.39 -        apply (tactic "smp_tac 3 1")
    1.40 -        apply (tactic "smp_tac 2 1")
    1.41 -        apply (tactic "smp_tac 1 1")
    1.42 +        apply (tactic "smp_tac @{context} 3 1")
    1.43 +        apply (tactic "smp_tac @{context} 2 1")
    1.44 +        apply (tactic "smp_tac @{context} 1 1")
    1.45          by blast
    1.46        moreover have "s1\<Colon>\<preceq>(G, L)"
    1.47        proof (cases "normal s0")
    1.48 @@ -2065,7 +2065,7 @@
    1.49                            (abupd (absorb (Cont l')) s2') \<diamondsuit> s3'"
    1.50                    apply (simp only: True if_True eqs)
    1.51                    apply (elim conjE)
    1.52 -                  apply (tactic "smp_tac 3 1")
    1.53 +                  apply (tactic "smp_tac @{context} 3 1")
    1.54                    apply fast
    1.55                    done
    1.56                  from eval_e