# HG changeset patch
# User huffman
# Date 1139452496 -3600
# Node ID 075550af9e11f481cd866a87cf8366d2fe565001
# Parent  a2950f74844586727d307ae1491a6cb7c0791741
removed redundant lemmas

diff -r a2950f748445 -r 075550af9e11 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Thu Feb 09 03:01:11 2006 +0100
+++ b/src/HOL/Real/Rational.thy	Thu Feb 09 03:34:56 2006 +0100
@@ -243,17 +243,6 @@
 
 subsubsection {* The ordered field of rational numbers *}
 
-lemma rat_add_assoc: "(q + r) + s = q + (r + (s::rat))"
-  by (induct q, induct r, induct s)
-     (simp add: add_rat add_ac mult_ac int_distrib)
-
-lemma rat_add_0: "0 + q = (q::rat)"
-  by (induct q) (simp add: zero_rat add_rat)
-
-lemma rat_left_minus: "(-q) + q = (0::rat)"
-  by (induct q) (simp add: zero_rat minus_rat add_rat eq_rat)
-
-
 instance rat :: field
 proof
   fix q r s :: rat