equal
deleted
inserted
replaced
7 |
7 |
8 Instantiation of the generic linear arithmetic package for type hypreal. |
8 Instantiation of the generic linear arithmetic package for type hypreal. |
9 *) |
9 *) |
10 |
10 |
11 (*FIXME DELETE*) |
11 (*FIXME DELETE*) |
|
12 val hypreal_mult_less_mono2 = thm"hypreal_mult_less_mono2"; |
|
13 |
12 val hypreal_mult_left_mono = |
14 val hypreal_mult_left_mono = |
13 read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; |
15 read_instantiate_sg(sign_of (the_context())) [("a","?a::hypreal")] mult_left_mono; |
14 |
16 |
15 |
17 |
16 val hypreal_number_of = thm "hypreal_number_of"; |
18 val hypreal_number_of = thm "hypreal_number_of"; |