changeset 14370 | b0064703967b |
parent 14369 | c50188fe6366 |
child 14387 | e96d5c42c4b0 |
--- 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;