diff -r caa2bbf8475d -r 315489d836d8 src/HOL/Semiring_Normalization.thy
--- a/src/HOL/Semiring_Normalization.thy	Tue Jun 11 18:33:27 2019 +0200
+++ b/src/HOL/Semiring_Normalization.thy	Fri Jun 14 08:34:27 2019 +0000
@@ -72,7 +72,7 @@
 context comm_semiring_1
 begin
 
-lemma semiring_normalization_rules:
+lemma semiring_normalization_rules [no_atp]:
   "(a * m) + (b * m) = (a + b) * m"
   "(a * m) + m = (a + 1) * m"
   "m + (a * m) = (a + 1) * m"
@@ -127,7 +127,7 @@
 context comm_ring_1
 begin
 
-lemma ring_normalization_rules:
+lemma ring_normalization_rules [no_atp]:
   "- x = (- 1) * x"
   "x - y = x + (- y)"
   by simp_all