changeset 48035 | 6a4c479ba94f |
parent 48034 | 248376f8881d |
child 48139 | 262d96552e50 |
1.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Mar 27 15:53:48 2012 +0200 1.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Tue Mar 27 16:04:51 2012 +0200 1.3 @@ -137,7 +137,7 @@ 1.4 lemma inv_inv: "zprime p \<Longrightarrow> 1.5 5 \<le> p \<Longrightarrow> 0 < a \<Longrightarrow> a < p ==> inv p (inv p a) = a" 1.6 apply (unfold inv_def) 1.7 - apply (subst zpower_zmod) 1.8 + apply (subst power_mod) 1.9 apply (subst zpower_zpower) 1.10 apply (rule zcong_zless_imp_eq) 1.11 prefer 5