equal
deleted
inserted
replaced
80 |
80 |
81 Goal "((number_of v :: real) = number_of v') = \ |
81 Goal "((number_of v :: real) = number_of v') = \ |
82 \ iszero (number_of (bin_add v (bin_minus v')))"; |
82 \ iszero (number_of (bin_add v (bin_minus v')))"; |
83 by (simp_tac |
83 by (simp_tac |
84 (HOL_ss addsimps [real_number_of_def, |
84 (HOL_ss addsimps [real_number_of_def, |
85 real_of_int_eq_iff, eq_number_of_eq]) 1); |
85 real_of_int_inject, eq_number_of_eq]) 1); |
86 qed "eq_real_number_of"; |
86 qed "eq_real_number_of"; |
87 |
87 |
88 Addsimps [eq_real_number_of]; |
88 Addsimps [eq_real_number_of]; |
89 |
89 |
90 (** Less-than (<) **) |
90 (** Less-than (<) **) |