src/HOLCF/ex/Focus_ex.thy
changeset 39159 0dec18004e75
parent 37598 893dcabf0c04
child 40002 c5b5f7a3a3b1
     1.1 --- a/src/HOLCF/ex/Focus_ex.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -180,7 +180,7 @@
     1.4  done
     1.5  
     1.6  lemma lemma3: "def_g(g) --> is_g(g)"
     1.7 -apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *})
     1.8 +apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
     1.9  apply (rule impI)
    1.10  apply (erule exE)
    1.11  apply (rule_tac x = "f" in exI)
    1.12 @@ -205,7 +205,7 @@
    1.13  
    1.14  lemma lemma4: "is_g(g) --> def_g(g)"
    1.15  apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
    1.16 -  addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
    1.17 +  addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *})
    1.18  apply (rule impI)
    1.19  apply (erule exE)
    1.20  apply (rule_tac x = "f" in exI)