equal
deleted
inserted
replaced
1 theory RealArith = RealArith0 |
1 theory RealArith = RealBin |
2 files ("real_arith.ML"): |
2 files ("real_arith.ML"): |
3 |
3 |
4 use "real_arith.ML" |
4 use "real_arith.ML" |
5 |
5 |
6 setup real_arith_setup |
6 setup real_arith_setup |
147 val real_less_half_sum = thm"real_less_half_sum"; |
147 val real_less_half_sum = thm"real_less_half_sum"; |
148 val real_gt_half_sum = thm"real_gt_half_sum"; |
148 val real_gt_half_sum = thm"real_gt_half_sum"; |
149 val real_dense = thm"real_dense"; |
149 val real_dense = thm"real_dense"; |
150 |
150 |
151 val abs_nat_number_of = thm"abs_nat_number_of"; |
151 val abs_nat_number_of = thm"abs_nat_number_of"; |
152 val abs_split = thm"abs_split"; |
|
153 val abs_zero = thm"abs_zero"; |
|
154 val abs_eqI1 = thm"abs_eqI1"; |
152 val abs_eqI1 = thm"abs_eqI1"; |
155 val abs_eqI2 = thm"abs_eqI2"; |
153 val abs_eqI2 = thm"abs_eqI2"; |
156 val abs_minus_eqI2 = thm"abs_minus_eqI2"; |
154 val abs_minus_eqI2 = thm"abs_minus_eqI2"; |
157 val abs_ge_zero = thm"abs_ge_zero"; |
155 val abs_ge_zero = thm"abs_ge_zero"; |
158 val abs_idempotent = thm"abs_idempotent"; |
156 val abs_idempotent = thm"abs_idempotent"; |