equal
deleted
inserted
replaced
6 Completeness theorems for positive reals and reals. |
6 Completeness theorems for positive reals and reals. |
7 *) |
7 *) |
8 |
8 |
9 claset_ref() := claset() delWrapper "bspec"; |
9 claset_ref() := claset() delWrapper "bspec"; |
10 |
10 |
11 Goal "x/# 2 + x/# 2 = (x::real)"; |
11 Goal "x/2 + x/2 = (x::real)"; |
12 by (Simp_tac 1); |
12 by (Simp_tac 1); |
13 qed "real_sum_of_halves"; |
13 qed "real_sum_of_halves"; |
14 |
14 |
15 (*--------------------------------------------------------- |
15 (*--------------------------------------------------------- |
16 Completeness of reals: use supremum property of |
16 Completeness of reals: use supremum property of |