src/HOL/Hyperreal/hypreal_arith.ML

--- a/src/HOL/Hyperreal/hypreal_arith.ML	Wed Jan 28 17:01:01 2004 +0100
+++ b/src/HOL/Hyperreal/hypreal_arith.ML	Thu Jan 29 16:51:17 2004 +0100
@@ -9,6 +9,8 @@
 *)
 
 (*FIXME DELETE*)
+val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2";
+
 val hypreal_mult_left_mono =
     read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono;