src/HOL/Number_Theory/Residues.thy
changeset 66888 930abfdf8727
parent 66837 6ba663ff2b1c
child 66954 0230af0f3c59
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Fri Oct 20 23:29:43 2017 +0200
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Fri Oct 20 20:57:55 2017 +0200
     1.3 @@ -112,7 +112,7 @@
     1.4       apply auto
     1.5     apply (metis invertible_coprime_int)
     1.6    apply (subst (asm) coprime_iff_invertible'_int)
     1.7 -   apply (auto simp add: cong_int_def mult.commute)
     1.8 +   apply (auto simp add: cong_def mult.commute)
     1.9    done
    1.10  
    1.11  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
    1.12 @@ -186,7 +186,7 @@
    1.13  qed
    1.14  
    1.15  lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
    1.16 -  by (auto simp: cong_int_def)
    1.17 +  by (auto simp: cong_def)
    1.18  
    1.19  
    1.20  text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close>
    1.21 @@ -364,7 +364,7 @@
    1.22      done
    1.23    finally have "fact (p - 1) mod p = \<ominus> \<one>" .
    1.24    then show ?thesis
    1.25 -    by (simp add: cong_int_def res_neg_eq res_one_eq zmod_int)
    1.26 +    by (simp add: cong_def res_neg_eq res_one_eq zmod_int)
    1.27  qed
    1.28  
    1.29  lemma wilson_theorem:
    1.30 @@ -373,7 +373,7 @@
    1.31  proof (cases "p = 2")
    1.32    case True
    1.33    then show ?thesis
    1.34 -    by (simp add: cong_int_def fact_prod)
    1.35 +    by (simp add: cong_def fact_prod)
    1.36  next
    1.37    case False
    1.38    then show ?thesis