equal
deleted
inserted
replaced
16 Goalw [real_number_of_def] "Numeral0 = (0::real)"; |
16 Goalw [real_number_of_def] "Numeral0 = (0::real)"; |
17 by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1); |
17 by (simp_tac (simpset() addsimps [real_of_int_zero RS sym]) 1); |
18 qed "real_numeral_0_eq_0"; |
18 qed "real_numeral_0_eq_0"; |
19 |
19 |
20 Goalw [real_number_of_def] "Numeral1 = (1::real)"; |
20 Goalw [real_number_of_def] "Numeral1 = (1::real)"; |
21 by (simp_tac (simpset() addsimps [real_of_int_one RS sym]) 1); |
21 by (stac (real_of_one RS sym) 1); |
|
22 by (Simp_tac 1); |
22 qed "real_numeral_1_eq_1"; |
23 qed "real_numeral_1_eq_1"; |
23 |
24 |
24 (** Addition **) |
25 (** Addition **) |
25 |
26 |
26 Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')"; |
27 Goal "(number_of v :: real) + number_of v' = number_of (bin_add v v')"; |