src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 39159 0dec18004e75
parent 38159 e9b4835a54ee
child 42793 88bee9f6eec7
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -257,7 +257,7 @@
     1.4     apply (subst wset.simps)
     1.5     apply (auto, unfold Let_def, auto)
     1.6    apply (subst setprod_insert)
     1.7 -    apply (tactic {* stac (thm "setprod_insert") 3 *})
     1.8 +    apply (tactic {* stac @{thm setprod_insert} 3 *})
     1.9        apply (subgoal_tac [5]
    1.10          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
    1.11         prefer 5