# HG changeset patch
# User huffman
# Date 1287274197 25200
# Node ID 9ee4e0ab29643730e031145981a2220153283f75
# Parent  98f2d8280eb4636589524c19d8baac10797433e0
remove old uses of 'simp_tac HOLCF_ss'

diff -r 98f2d8280eb4 -r 9ee4e0ab2964 src/HOLCF/ex/Focus_ex.thy
--- 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)
diff -r 98f2d8280eb4 -r 9ee4e0ab2964 src/HOLCF/ex/Hoare.thy
--- 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   ----- *)
diff -r 98f2d8280eb4 -r 9ee4e0ab2964 src/HOLCF/ex/Loop.thy
--- 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)