# HG changeset patch
# User bauerg
# Date 975589823 -3600
# Node ID 71eb53f36878a862642f54959cba507bf95ee3ba
# Parent  8e4307d1207ae36a7226388ed93b3c23c4138702
some properties;

diff -r 8e4307d1207a -r 71eb53f36878 src/HOL/Library/Ring_and_Field.thy
--- a/src/HOL/Library/Ring_and_Field.thy	Thu Nov 30 13:56:46 2000 +0100
+++ b/src/HOL/Library/Ring_and_Field.thy	Thu Nov 30 14:10:23 2000 +0100
@@ -16,7 +16,7 @@
   add_assoc: "(a + b) + c = a + (b + c)"
   add_commute: "a + b = b + a"
   left_zero: "0 + a = a"
-  left_minus: "(-a) + a = 0"
+  right_minus: "a + - a = 0"
   diff_minus: "a - b = a + (-b)"
   zero_number: "0 = #0"
 
@@ -37,6 +37,13 @@
 
 axclass ordered_field < ordered_ring, field
 
+subsection {* simplification rules *}
+
+lemma left_minus [simp]: "- (a::'a::field) + a = 0"
+  by (simp only: add_commute right_minus)
+
+lemma diff_self [simp]: "a - (a::'a::field) = 0"
+  by (simp only: diff_minus right_minus)
 
 subsection {* The ordered ring of integers *}
 
@@ -46,7 +53,7 @@
   show "(i + j) + k = i + (j + k)" by simp
   show "i + j = j + i" by simp
   show "0 + i = i" by simp
-  show "(-i) + i = 0" by simp
+  show "i + - i = 0" by simp
   show "i - j = i + (-j)" by simp
   show "(i * j) * k = i * (j * k)" by simp
   show "i * j = j * i" by simp