src/HOL/NumberTheory/IntPrimes.thy

   done
 
 lemma zcong_trans:
     "[a = b] (mod m) ==> [b = c] (mod m) ==> [a = c] (mod m)"
   unfolding zcong_def
-  apply (auto elim!: dvdE simp add: ring_simps)
+  apply (auto elim!: dvdE simp add: algebra_simps)
   unfolding left_distrib [symmetric]
   apply (rule dvd_mult dvd_refl)+
   done
 
 lemma zcong_zmult:

   apply (metis zmult_div_cancel)
   done
 
 lemma zcong_iff_lin: "([a = b] (mod m)) = (\<exists>k. b = a + m * k)"
   unfolding zcong_def
-  apply (auto elim!: dvdE simp add: ring_simps)
+  apply (auto elim!: dvdE simp add: algebra_simps)
   apply (rule_tac x = "-k" in exI) apply simp
   done
 
 lemma zgcd_zcong_zgcd:
   "0 < m ==>