# HG changeset patch
# User nipkow
# Date 1021456280 -7200
# Node ID 0f1c6fa846f23645e85dab89c9cf8ab1e746e6ea
# Parent  0c50d13d449a27d3be2dd914e39e32fd4ef09bde
Removed superfluous thm

diff -r 0c50d13d449a -r 0f1c6fa846f2 src/HOL/Hyperreal/EvenOdd.ML
--- a/src/HOL/Hyperreal/EvenOdd.ML	Wed May 15 10:44:58 2002 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.ML	Wed May 15 11:51:20 2002 +0200
@@ -102,11 +102,6 @@
 qed "even_mult_even";
 Addsimps [even_mult_even];
 
-Goal "(m*2) div 2 = (m::nat)";
-by (rtac div_mult_self_is_m 1);
-by (Simp_tac 1);
-qed "div_mult_self_two_is_m";
-
 Goal "(m + m) div 2 = (m::nat)";
 by (asm_full_simp_tac (simpset() addsimps [m_add_m_eq2]) 1); 
 qed "div_add_self_two_is_m";