src/HOLCF/IOA/meta_theory/RefCorrectness.thy

 lemma lemma_1:
   "[|is_ref_map f C A; ext C = ext A|] ==>
          !s. reachable C s & is_exec_frag C (s,xs) -->
              mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
 apply (unfold corresp_ex_def)
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
 (* cons case *)
 apply (auto simp add: mk_traceConc)
 apply (frule reachable.reachable_n)
 apply assumption
 apply (erule_tac x = "y" in allE)

  (!s .is_exec_frag A (s,xs) & is_exec_frag A (t,ys) &
       t = laststate (s,xs)
   --> is_exec_frag A (s,xs @@ ys))"
 
 apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac 1 *})
+apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
 (* main case *)
 apply (auto simp add: split_paired_all)
 done
 
 

   --> is_exec_frag A (corresp_ex A f (s,xs))"
 
 apply (unfold corresp_ex_def)
 
 apply simp
-apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
+apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
 (* main case *)
 apply auto
 apply (rule_tac t = "f y" in lemma_2_1)
 
 (* Finite *)

 
   (* give execution of abstract automata *)
   apply (rule_tac x = "corresp_ex A f ex" in bexI)
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
   apply (simp add: is_ref_map_def corresp_ex_def)
   (* is-execution-fragment *)

 apply auto
 apply (rule_tac x = "corresp_ex A f ex" in exI)
 apply auto
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
   apply (simp add: is_ref_map_def corresp_ex_def)
   (* is-execution-fragment *)

 apply auto
 apply (rule_tac x = "corresp_ex A f ex" in exI)
 apply auto
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac "ex" 1 *})
+  apply (tactic {* pair_tac @{context} "ex" 1 *})
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
   apply (simp add: is_ref_map_def corresp_ex_def)
   (* is-execution-fragment *)
   apply (erule lemma_2 [THEN spec, THEN mp])
   apply (simp add: reachable.reachable_0)
 
 done
 
-
 end