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
```