diff -r f3763989d589 -r 5b269897df9d src/HOL/Number_Theory/Quadratic_Reciprocity.thy
--- a/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Jul 29 18:24:47 2018 +0200
+++ b/src/HOL/Number_Theory/Quadratic_Reciprocity.thy	Sun Jul 29 23:04:22 2018 +0100
@@ -93,7 +93,7 @@
 
 lemma Gpq: "GAUSS p q"
   using p_prime pq_neq p_ge_2 q_prime
-  by (auto simp: GAUSS_def cong_altdef_int dest: primes_dvd_imp_eq)
+  by (auto simp: GAUSS_def cong_iff_dvd_diff dest: primes_dvd_imp_eq)
 
 lemma Gqp: "GAUSS q p"
   by (simp add: QRqp QR.Gpq)
@@ -304,7 +304,7 @@
   by (simp add: f_2_def)
 
 lemma f_2_lemma_2: "[f_2 x = int p - x] (mod p)"
-  by (simp add: f_2_def cong_altdef_int)
+  by (simp add: f_2_def cong_iff_dvd_diff)
 
 lemma f_2_lemma_3: "f_2 x \<in> S \<Longrightarrow> x \<in> f_2 ` S"
   using f_2_lemma_1[of x] image_eqI[of x f_2 "f_2 x" S] by presburger