# HG changeset patch
# User wenzelm
# Date 976136929 -3600
# Node ID 3d15596ee644bac7064a122a8b055c5a767e2d3e
# Parent  ef6c65d992b61265b23faee69bfa5fb75f90b72b
left_minus axiom;

diff -r ef6c65d992b6 -r 3d15596ee644 src/HOL/Library/Rational_Numbers.thy
--- a/src/HOL/Library/Rational_Numbers.thy	Wed Dec 06 21:53:05 2000 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy	Wed Dec 06 22:08:49 2000 +0100
@@ -488,7 +488,7 @@
     by (induct q, induct r) (simp add: add_rat zadd_ac zmult_ac)
   show "0 + q = q"
     by (induct q) (simp add: zero_rat add_rat)
-  show "q + (-q) = 0"
+  show "(-q) + q = 0"
     by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
   show "q - r = q + (-r)"
     by (induct q, induct r) (simp add: add_rat minus_rat diff_rat)