avoid spammed sledgehammer proofs
authorhaftmann
Fri Jun 14 08:34:27 2019 +0000 (5 weeks ago)
changeset 70332315489d836d8
parent 70331 caa2bbf8475d
child 70333 0f7edf0853df
avoid spammed sledgehammer proofs
src/HOL/Semiring_Normalization.thy
     1.1 --- a/src/HOL/Semiring_Normalization.thy	Tue Jun 11 18:33:27 2019 +0200
     1.2 +++ b/src/HOL/Semiring_Normalization.thy	Fri Jun 14 08:34:27 2019 +0000
     1.3 @@ -72,7 +72,7 @@
     1.4  context comm_semiring_1
     1.5  begin
     1.6  
     1.7 -lemma semiring_normalization_rules:
     1.8 +lemma semiring_normalization_rules [no_atp]:
     1.9    "(a * m) + (b * m) = (a + b) * m"
    1.10    "(a * m) + m = (a + 1) * m"
    1.11    "m + (a * m) = (a + 1) * m"
    1.12 @@ -127,7 +127,7 @@
    1.13  context comm_ring_1
    1.14  begin
    1.15  
    1.16 -lemma ring_normalization_rules:
    1.17 +lemma ring_normalization_rules [no_atp]:
    1.18    "- x = (- 1) * x"
    1.19    "x - y = x + (- y)"
    1.20    by simp_all