src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 57418 6ab1c7cb0b8d
parent 47268 262d96552e50
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Fri Jun 27 22:08:55 2014 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Jun 28 09:16:42 2014 +0200
     1.3 @@ -251,8 +251,8 @@
     1.4     prefer 2
     1.5     apply (subst wset.simps)
     1.6     apply (auto, unfold Let_def, auto)
     1.7 -  apply (subst setprod_insert)
     1.8 -    apply (tactic {* stac @{thm setprod_insert} 3 *})
     1.9 +  apply (subst setprod.insert)
    1.10 +    apply (tactic {* stac @{thm setprod.insert} 3 *})
    1.11        apply (subgoal_tac [5]
    1.12          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
    1.13         prefer 5