changeset 54230 | b1d955791529 |
parent 53076 | 47c9aff07725 |
child 57514 | bdc2c6b40bf2 |
--- a/src/HOL/Semiring_Normalization.thy Thu Oct 31 16:54:22 2013 +0100 +++ b/src/HOL/Semiring_Normalization.thy Fri Nov 01 18:51:14 2013 +0100 @@ -137,7 +137,7 @@ lemma normalizing_ring_rules: "- x = (- 1) * x" "x - y = x + (- y)" - by (simp_all add: diff_minus) + by simp_all lemmas normalizing_comm_ring_1_axioms = comm_ring_1_axioms [normalizer