--- a/src/HOL/Hyperreal/HyperBin.ML Thu Jan 04 10:22:33 2001 +0100
+++ b/src/HOL/Hyperreal/HyperBin.ML Thu Jan 04 10:23:01 2001 +0100
@@ -172,15 +172,6 @@
hypreal_add_number_of_diff1, hypreal_add_number_of_diff2];
-(*"neg" is used in rewrite rules for binary comparisons*)
-Goal "hypreal_of_nat (number_of v :: nat) = \
-\ (if neg (number_of v) then #0 \
-\ else (number_of v :: hypreal))";
-by (simp_tac (simpset() addsimps [hypreal_of_nat_real_of_nat]) 1);
-qed "hypreal_of_nat_number_of";
-Addsimps [hypreal_of_nat_number_of];
-
-
(**** Simprocs for numeric literals ****)
(** Combining of literal coefficients in sums of products **)