src/HOL/Number_Theory/Residues.thy
changeset 63417 c184ec919c70
parent 63167 0909deb8059b
child 63534 523b488b15c9
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Jul 08 23:43:11 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Jul 09 13:26:16 2016 +0200
     1.3 @@ -426,7 +426,7 @@
     1.4      apply auto
     1.5      done
     1.6    also have "\<dots> = fact (p - 1) mod p"
     1.7 -    apply (subst fact_altdef_nat)
     1.8 +    apply (simp add: fact_setprod)
     1.9      apply (insert assms)
    1.10      apply (subst res_prime_units_eq)
    1.11      apply (simp add: int_setprod zmod_int setprod_int_eq)
    1.12 @@ -443,7 +443,7 @@
    1.13  proof (cases "p = 2")
    1.14    case True
    1.15    then show ?thesis
    1.16 -    by (simp add: cong_int_def fact_altdef_nat)
    1.17 +    by (simp add: cong_int_def fact_setprod)
    1.18  next
    1.19    case False
    1.20    then show ?thesis