equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 (*FIXME DELETE*) |
11 (*FIXME DELETE*) |
12 val real_mult_left_mono = |
12 val real_mult_left_mono = |
13 read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono; |
13 read_instantiate_sg(sign_of (the_context())) [("a","?a::real")] mult_left_mono; |
14 |
|
15 val real_abs_def = thm "real_abs_def"; |
|
16 |
14 |
17 val real_le_def = thm "real_le_def"; |
15 val real_le_def = thm "real_le_def"; |
18 val real_diff_def = thm "real_diff_def"; |
16 val real_diff_def = thm "real_diff_def"; |
19 val real_divide_def = thm "real_divide_def"; |
17 val real_divide_def = thm "real_divide_def"; |
20 |
18 |