# HG changeset patch
# User huffman
# Date 1321209035 -3600
# Node ID cf937a9ce051ce11af05b2e5b87d8651a4e3579a
# Parent  a39bb6d42acebb86752483ff801580e10114db41
remove lemma float_remove_real_numeral, which duplicated Float.float_number_of

diff -r a39bb6d42ace -r cf937a9ce051 src/HOL/Decision_Procs/Approximation.thy
--- a/src/HOL/Decision_Procs/Approximation.thy	Sun Nov 13 19:26:53 2011 +0100
+++ b/src/HOL/Decision_Procs/Approximation.thy	Sun Nov 13 19:30:35 2011 +0100
@@ -1178,15 +1178,6 @@
   from *[OF this] show thesis by blast
 qed
 
-lemma float_remove_real_numeral[simp]: "(number_of k :: float) = (number_of k :: real)"
-proof -
-  have "(number_of k :: float) = real k"
-    unfolding number_of_float_def real_of_float_def pow2_def by auto
-  also have "\<dots> = (number_of k :: int)"
-    by (simp add: number_of_is_id)
-  finally show ?thesis by auto
-qed
-
 lemma cos_periodic_nat[simp]: fixes n :: nat shows "cos (x + n * (2 * pi)) = cos x"
 proof (induct n arbitrary: x)
   case (Suc n)