src/HOLCF/IOA/meta_theory/TLS.thy

 declare ex2seqC_UU [simp del] ex2seqC_nil [simp del] ex2seqC_cons [simp del]
 declare ex2seq_UU [simp] ex2seq_nil [simp] ex2seq_cons [simp]
 
 
 lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
-apply (tactic {* pair_tac "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "exec" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 done
 
 
 subsection {* Interface TL -- TLS *}
 

 
 apply clarify
 apply (simp split add: split_if)
 (* TL = UU *)
 apply (rule conjI)
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 (* TL = nil *)
 apply (rule conjI)
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_tac "y" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_tac @{context} "y" 1 *})
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
 (* TL =cons *)
 apply (simp add: unlift_def)
 
-apply (tactic {* pair_tac "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac "y" 1 *})
-apply (tactic {* pair_tac "a" 1 *})
-apply (tactic {* Seq_case_simp_tac "s" 1 *})
+apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "y" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
 apply blast
 apply fastsimp
-apply (tactic {* pair_tac "a" 1 *})
+apply (tactic {* pair_tac @{context} "a" 1 *})
  apply fastsimp
 done
 
 end