src/HOL/Old_Number_Theory/WilsonRuss.thy
changeset 32960 69916a850301
parent 32479 521cc9bf2958
child 35048 82ab78fff970
     1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 17 01:05:59 2009 +0200
     1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Sat Oct 17 14:43:18 2009 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4        apply (subst zcong_zmod [symmetric])
     1.5        apply (subst inv_inv_aux)
     1.6         apply (subgoal_tac [2]
     1.7 -	 "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
     1.8 +         "zcong (a * a^(nat (p - 1) * nat (p - 3))) (a * 1) p")
     1.9          apply (rule_tac [3] zcong_zmult)
    1.10           apply (rule_tac [4] zcong_zpower_zmult)
    1.11           apply (erule_tac [4] Little_Fermat)
    1.12 @@ -263,7 +263,7 @@
    1.13    apply (subst setprod_insert)
    1.14      apply (tactic {* stac (thm "setprod_insert") 3 *})
    1.15        apply (subgoal_tac [5]
    1.16 -	"zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
    1.17 +        "zcong (a * inv p a * (\<Prod>x\<in> wset(a - 1, p). x)) (1 * 1) p")
    1.18         prefer 5
    1.19         apply (simp add: zmult_assoc)
    1.20        apply (rule_tac [5] zcong_zmult)