src/HOLCF/ex/Focus_ex.thy
changeset 40028 9ee4e0ab2964
parent 40002 c5b5f7a3a3b1
     1.1 --- a/src/HOLCF/ex/Focus_ex.thy	Sat Oct 16 16:39:06 2010 -0700
     1.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Sat Oct 16 17:09:57 2010 -0700
     1.3 @@ -160,9 +160,9 @@
     1.4  apply (rule_tac [2] conjI)
     1.5  prefer 3 apply (assumption)
     1.6  apply (drule sym)
     1.7 -apply (tactic "asm_simp_tac HOLCF_ss 1")
     1.8 +apply (simp)
     1.9  apply (drule sym)
    1.10 -apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.11 +apply (simp)
    1.12  apply (erule exE)
    1.13  apply (rule_tac x = "f" in exI)
    1.14  apply (erule conjE)+
    1.15 @@ -189,7 +189,7 @@
    1.16  apply (intro strip)
    1.17  apply (rule_tac x = "fix$ (LAM k. snd (f$(x,k)))" in exI)
    1.18  apply (rule conjI)
    1.19 - apply (tactic "asm_simp_tac HOLCF_ss 1")
    1.20 + apply (simp)
    1.21   apply (rule prod_eqI, simp, simp)
    1.22   apply (rule trans)
    1.23    apply (rule fix_eq)
    1.24 @@ -220,9 +220,6 @@
    1.25  apply (subgoal_tac "! w y. f$(x, w) = (y, w) --> z << w")
    1.26  apply (rule fix_eqI)
    1.27  apply simp
    1.28 -(*apply (rule allI)*)
    1.29 -(*apply (tactic "simp_tac HOLCF_ss 1")*)
    1.30 -(*apply (intro strip)*)
    1.31  apply (subgoal_tac "f$(x, za) = (fst (f$(x,za)) ,za)")
    1.32  apply fast
    1.33  apply (rule prod_eqI, simp, simp)