src/HOL/IMPP/Hoare.thy

 apply             (fast intro: hoare_derivs.cut)
 apply            (fast intro: hoare_derivs.weaken)
 apply           (rule hoare_derivs.conseq, intro strip, tactic "smp_tac @{context} 2 1", clarify, tactic "smp_tac @{context} 1 1",rule exI, rule exI, erule (1) conjI)
 prefer 7
 apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
-apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
+apply         (tactic {* ALLGOALS (resolve_tac @{context} ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{context})) *})
 done
 
 lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
 apply (rule BodyN)
 apply (erule thin)

 apply (fast intro!: Body_triple_valid_Suc [THEN iffD1])
 done
 
 lemma hoare_sound: "G||-ts ==> G||=ts"
 apply (erule hoare_derivs.induct)
-apply              (tactic {* TRYALL (eresolve_tac [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *})
+apply              (tactic {* TRYALL (eresolve_tac @{context} [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *})
 apply            (unfold hoare_valids_def)
 apply            blast
 apply           blast
 apply          (blast) (* asm *)
 apply         (blast) (* cut *)