equal
deleted
inserted
replaced
781 by (transfer, rule refl) |
781 by (transfer, rule refl) |
782 |
782 |
783 |
783 |
784 subsection{*Numerals and Arithmetic*} |
784 subsection{*Numerals and Arithmetic*} |
785 |
785 |
786 lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int (Rep_Bin w)" |
786 lemma hcomplex_number_of_def: "(number_of w :: hcomplex) == of_int w" |
787 by (transfer, rule number_of_eq [THEN eq_reflection]) |
787 by (transfer, rule number_of_eq [THEN eq_reflection]) |
788 |
788 |
789 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
789 lemma hcomplex_of_hypreal_eq_hcomplex_of_complex: |
790 "hcomplex_of_hypreal (hypreal_of_real x) = |
790 "hcomplex_of_hypreal (hypreal_of_real x) = |
791 hcomplex_of_complex (complex_of_real x)" |
791 hcomplex_of_complex (complex_of_real x)" |