--- a/src/HOLCF/ex/Focus_ex.thy Sat Oct 16 16:39:06 2010 -0700
+++ b/src/HOLCF/ex/Focus_ex.thy Sat Oct 16 17:09:57 2010 -0700
@@ -160,9 +160,9 @@
apply (rule_tac [2] conjI)
prefer 3 apply (assumption)
apply (drule sym)
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply (drule sym)
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply (erule exE)
apply (rule_tac x = "f" in exI)
apply (erule conjE)+
@@ -189,7 +189,7 @@
apply (intro strip)
apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI)
apply (rule conjI)
- apply (tactic "asm_simp_tac HOLCF_ss 1")
+ apply (simp)
apply (rule prod_eqI, simp, simp)
apply (rule trans)
apply (rule fix_eq)
@@ -220,9 +220,6 @@
apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w")
apply (rule fix_eqI)
apply simp
-(*apply (rule allI)*)
-(*apply (tactic "simp_tac HOLCF_ss 1")*)
-(*apply (intro strip)*)
apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)")
apply fast
apply (rule prod_eqI, simp, simp)
--- a/src/HOLCF/ex/Hoare.thy Sat Oct 16 16:39:06 2010 -0700
+++ b/src/HOLCF/ex/Hoare.thy Sat Oct 16 17:09:57 2010 -0700
@@ -188,7 +188,7 @@
apply assumption
apply assumption
apply (simp (no_asm))
-apply (tactic "simp_tac HOLCF_ss 1")
+apply (simp (no_asm))
apply (rule trans)
apply (rule p_def3)
apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric])
@@ -222,7 +222,7 @@
apply assumption
apply assumption
apply (simp (no_asm))
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply (rule trans)
apply (rule p_def3)
apply simp
@@ -238,7 +238,7 @@
apply (rule allI)
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
apply (erule spec)
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply (rule iterate_Suc [THEN subst])
apply (erule spec)
done
@@ -258,7 +258,7 @@
apply (simp (no_asm))
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
apply (erule spec)
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply (rule iterate_Suc [THEN subst])
apply (erule spec)
done
@@ -283,7 +283,7 @@
apply (simp (no_asm))
apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
apply (erule spec)
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply (rule iterate_Suc [THEN subst])
apply (erule spec)
done
@@ -338,7 +338,7 @@
apply (intro strip)
apply (erule conjE)
apply (subst q_def3)
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply hypsubst
apply (simp (no_asm))
apply (intro strip)
@@ -354,10 +354,10 @@
apply assumption
apply assumption
apply (simp (no_asm))
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
apply (rule trans)
apply (rule q_def3)
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp)
done
(* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q ----- *)
--- a/src/HOLCF/ex/Loop.thy Sat Oct 16 16:39:06 2010 -0700
+++ b/src/HOLCF/ex/Loop.thy Sat Oct 16 17:09:57 2010 -0700
@@ -104,12 +104,11 @@
apply (simp (no_asm) add: step_def2)
apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
apply (erule notE)
-apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [@{thm step_def2}]) 1 *})
-apply (tactic "asm_simp_tac HOLCF_ss 1")
+apply (simp add: step_def2)
+apply (simp (no_asm_simp))
apply (rule mp)
apply (erule spec)
-apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}]
- addsimps [@{thm loop_lemma2}]) 1 *})
+apply (simp (no_asm_simp) del: iterate_Suc add: loop_lemma2)
apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
prefer 2 apply (assumption)