# HG changeset patch
# User haftmann
# Date 1192772903 -7200
# Node ID 04b8456f775447b30223eeea276416e52965e92a
# Parent  9a13ab12b174b75ef990119ca2ac4120925c7bcc
dropped doubled proof

diff -r 9a13ab12b174 -r 04b8456f7754 src/HOL/Numeral.thy
--- a/src/HOL/Numeral.thy	Thu Oct 18 17:44:30 2007 +0200
+++ b/src/HOL/Numeral.thy	Fri Oct 19 07:48:23 2007 +0200
@@ -325,13 +325,7 @@
 
 subsection {* Comparisons, for Ordered Rings *}
 
-lemma double_eq_0_iff:
-  "(a + a = 0) = (a = (0::'a::ordered_idom))"
-proof -
-  have "a + a = (1 + 1) * a" unfolding left_distrib by simp
-  with zero_less_two [where 'a = 'a]
-  show ?thesis by force
-qed
+lemmas double_eq_0_iff = double_zero
 
 lemma le_imp_0_less: 
   assumes le: "0 \<le> z"