--- a/src/HOL/Number_Theory/Gauss.thy Sun Jan 13 20:25:41 2019 +0100
+++ b/src/HOL/Number_Theory/Gauss.thy Mon Jan 14 14:46:12 2019 +0100
@@ -339,7 +339,7 @@
theorem pre_gauss_lemma: "[a ^ nat((int p - 1) div 2) = (-1) ^ (card E)] (mod p)"
proof -
have "[prod id A = prod id F * prod id D](mod p)"
- by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_strong)
+ by (auto simp: prod_D_F_eq_prod_A mult.commute cong del: prod.cong_simp)
then have "[prod id A = ((-1)^(card E) * prod id E) * prod id D] (mod p)"
by (rule cong_trans) (metis cong_scalar_right prod_F_zcong)
then have "[prod id A = ((-1)^(card E) * prod id C)] (mod p)"
@@ -364,7 +364,7 @@
(-1)^(card E) * a^(card A) * (-1)^(card E)](mod p)"
by (rule cong_trans) (simp add: a ac_simps)
then have "[prod id A * (-1)^(card E) = prod id A * a^(card A)](mod p)"
- by (rule cong_trans) (simp add: aux cong del: prod.cong_strong)
+ by (rule cong_trans) (simp add: aux cong del: prod.cong_simp)
with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
by (metis cong_mult_lcancel)
then show ?thesis