src/HOLCF/ex/Hoare.thy
changeset 40028 9ee4e0ab2964
parent 40002 c5b5f7a3a3b1
child 40322 707eb30e8a53
     1.1 --- a/src/HOLCF/ex/Hoare.thy	Sat Oct 16 16:39:06 2010 -0700
     1.2 +++ b/src/HOLCF/ex/Hoare.thy	Sat Oct 16 17:09:57 2010 -0700
     1.3 @@ -188,7 +188,7 @@
     1.4  apply assumption
     1.5  apply assumption
     1.6  apply (simp (no_asm))
     1.7 -apply (tactic "simp_tac HOLCF_ss 1")
     1.8 +apply (simp (no_asm))
     1.9  apply (rule trans)
    1.10  apply (rule p_def3)
    1.11  apply (simp (no_asm) del: iterate_Suc add: iterate_Suc [symmetric])
    1.12 @@ -222,7 +222,7 @@
    1.13  apply assumption
    1.14  apply assumption
    1.15  apply (simp (no_asm))
    1.16 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.17 +apply (simp)
    1.18  apply (rule trans)
    1.19  apply (rule p_def3)
    1.20  apply simp
    1.21 @@ -238,7 +238,7 @@
    1.22  apply (rule allI)
    1.23  apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
    1.24  apply (erule spec)
    1.25 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.26 +apply (simp)
    1.27  apply (rule iterate_Suc [THEN subst])
    1.28  apply (erule spec)
    1.29  done
    1.30 @@ -258,7 +258,7 @@
    1.31  apply (simp (no_asm))
    1.32  apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$x) " in ssubst)
    1.33  apply (erule spec)
    1.34 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.35 +apply (simp)
    1.36  apply (rule iterate_Suc [THEN subst])
    1.37  apply (erule spec)
    1.38  done
    1.39 @@ -283,7 +283,7 @@
    1.40  apply (simp (no_asm))
    1.41  apply (rule_tac s = "TT" and t = "b1$ (iterate k$g$ (x::'a))" in ssubst)
    1.42  apply (erule spec)
    1.43 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.44 +apply (simp)
    1.45  apply (rule iterate_Suc [THEN subst])
    1.46  apply (erule spec)
    1.47  done
    1.48 @@ -338,7 +338,7 @@
    1.49  apply (intro strip)
    1.50  apply (erule conjE)
    1.51  apply (subst q_def3)
    1.52 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.53 +apply (simp)
    1.54  apply hypsubst
    1.55  apply (simp (no_asm))
    1.56  apply (intro strip)
    1.57 @@ -354,10 +354,10 @@
    1.58  apply assumption
    1.59  apply assumption
    1.60  apply (simp (no_asm))
    1.61 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.62 +apply (simp)
    1.63  apply (rule trans)
    1.64  apply (rule q_def3)
    1.65 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.66 +apply (simp)
    1.67  done
    1.68  
    1.69  (* ------- (ALL k. b1$(iterate k$g$x)=TT) ==> q o p = q   ----- *)