src/HOL/Number_Theory/Residues.thy
changeset 64272 f76b6dda2e56
parent 63633 2accfb71e33b
child 64282 261d42f0bfac
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Mon Oct 17 14:37:32 2016 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Mon Oct 17 17:33:07 2016 +0200
     1.3 @@ -428,10 +428,10 @@
     1.4      apply auto
     1.5      done
     1.6    also have "\<dots> = fact (p - 1) mod p"
     1.7 -    apply (simp add: fact_setprod)
     1.8 +    apply (simp add: fact_prod)
     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 +    apply (simp add: int_prod zmod_int prod_int_eq)
    1.13      done
    1.14    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
    1.15    then show ?thesis
    1.16 @@ -445,7 +445,7 @@
    1.17  proof (cases "p = 2")
    1.18    case True
    1.19    then show ?thesis
    1.20 -    by (simp add: cong_int_def fact_setprod)
    1.21 +    by (simp add: cong_int_def fact_prod)
    1.22  next
    1.23    case False
    1.24    then show ?thesis