42 val real_less_all_real2 = thm "real_less_all_real2"; |
42 val real_less_all_real2 = thm "real_less_all_real2"; |
43 val real_of_preal_le_iff = thm "real_of_preal_le_iff"; |
43 val real_of_preal_le_iff = thm "real_of_preal_le_iff"; |
44 val real_mult_order = thm "real_mult_order"; |
44 val real_mult_order = thm "real_mult_order"; |
45 val real_add_order = thm "real_add_order"; |
45 val real_add_order = thm "real_add_order"; |
46 val real_le_add_order = thm "real_le_add_order"; |
46 val real_le_add_order = thm "real_le_add_order"; |
47 val real_le_square = thm "real_le_square"; |
|
48 val real_mult_less_mono2 = thm "real_mult_less_mono2"; |
47 val real_mult_less_mono2 = thm "real_mult_less_mono2"; |
49 |
48 |
50 val real_mult_less_iff1 = thm "real_mult_less_iff1"; |
49 val real_mult_less_iff1 = thm "real_mult_less_iff1"; |
51 val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; |
50 val real_mult_le_cancel_iff1 = thm "real_mult_le_cancel_iff1"; |
52 val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; |
51 val real_mult_le_cancel_iff2 = thm "real_mult_le_cancel_iff2"; |
53 val real_mult_less_mono = thm "real_mult_less_mono"; |
52 val real_mult_less_mono = thm "real_mult_less_mono"; |
54 val real_sum_squares_cancel = thm "real_sum_squares_cancel"; |
|
55 val real_sum_squares_cancel2 = thm "real_sum_squares_cancel2"; |
|
56 |
53 |
57 val real_mult_left_cancel = thm"real_mult_left_cancel"; |
54 val real_mult_left_cancel = thm"real_mult_left_cancel"; |
58 val real_mult_right_cancel = thm"real_mult_right_cancel"; |
55 val real_mult_right_cancel = thm"real_mult_right_cancel"; |
59 val real_inverse_unique = thm "real_inverse_unique"; |
56 val real_inverse_unique = thm "real_inverse_unique"; |
60 val real_inverse_gt_one = thm "real_inverse_gt_one"; |
57 val real_inverse_gt_one = thm "real_inverse_gt_one"; |