--- a/src/HOLCF/IOA/meta_theory/TLS.thy Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.thy Sat Jun 14 23:19:51 2008 +0200
@@ -149,9 +149,9 @@
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
@@ -170,33 +170,33 @@
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