src/HOL/Old_Number_Theory/WilsonBij.thy
changeset 39159 0dec18004e75
parent 38159 e9b4835a54ee
child 44766 d4d33a4d7548
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -145,9 +145,9 @@
     1.4    apply (unfold inj_on_def)
     1.5    apply auto
     1.6    apply (rule zcong_zless_imp_eq)
     1.7 -      apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *})
     1.8 +      apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *})
     1.9          apply (rule_tac [7] zcong_trans)
    1.10 -         apply (tactic {* stac (thm "zcong_sym") 8 *})
    1.11 +         apply (tactic {* stac @{thm zcong_sym} 8 *})
    1.12           apply (erule_tac [7] inv_is_inv)
    1.13            apply (tactic "asm_simp_tac @{simpset} 9")
    1.14            apply (erule_tac [9] inv_is_inv)
    1.15 @@ -198,15 +198,15 @@
    1.16    apply (unfold reciR_def uniqP_def)
    1.17    apply auto
    1.18     apply (rule zcong_zless_imp_eq)
    1.19 -       apply (tactic {* stac (thm "zcong_cancel2" RS sym) 5 *})
    1.20 +       apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 5 *})
    1.21           apply (rule_tac [7] zcong_trans)
    1.22 -          apply (tactic {* stac (thm "zcong_sym") 8 *})
    1.23 +          apply (tactic {* stac @{thm zcong_sym} 8 *})
    1.24            apply (rule_tac [6] zless_zprime_imp_zrelprime)
    1.25              apply auto
    1.26    apply (rule zcong_zless_imp_eq)
    1.27 -      apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *})
    1.28 +      apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *})
    1.29          apply (rule_tac [7] zcong_trans)
    1.30 -         apply (tactic {* stac (thm "zcong_sym") 8 *})
    1.31 +         apply (tactic {* stac @{thm zcong_sym} 8 *})
    1.32           apply (rule_tac [6] zless_zprime_imp_zrelprime)
    1.33             apply auto
    1.34    done