equal
deleted
inserted
replaced
68 qed "complex_mult_2_right"; |
68 qed "complex_mult_2_right"; |
69 |
69 |
70 (** Equals (=) **) |
70 (** Equals (=) **) |
71 |
71 |
72 Goal "((number_of v :: complex) = number_of v') = \ |
72 Goal "((number_of v :: complex) = number_of v') = \ |
73 \ iszero (number_of (bin_add v (bin_minus v')))"; |
73 \ iszero (number_of (bin_add v (bin_minus v')) :: int)"; |
74 by (simp_tac |
74 by (simp_tac |
75 (HOL_ss addsimps [complex_number_of_def, |
75 (HOL_ss addsimps [complex_number_of_def, |
76 complex_of_real_eq_iff, eq_real_number_of]) 1); |
76 complex_of_real_eq_iff, eq_real_number_of]) 1); |
77 qed "eq_complex_number_of"; |
77 qed "eq_complex_number_of"; |
78 Addsimps [eq_complex_number_of]; |
78 Addsimps [eq_complex_number_of]; |