equal
deleted
inserted
replaced
828 subsection{*Numerals and Arithmetic*} |
828 subsection{*Numerals and Arithmetic*} |
829 |
829 |
830 instance complex :: number .. |
830 instance complex :: number .. |
831 |
831 |
832 defs (overloaded) |
832 defs (overloaded) |
833 complex_number_of_def: "(number_of w :: complex) == of_int (Rep_Bin w)" |
833 complex_number_of_def: "(number_of w :: complex) == of_int w" |
834 --{*the type constraint is essential!*} |
834 --{*the type constraint is essential!*} |
835 |
835 |
836 instance complex :: number_ring |
836 instance complex :: number_ring |
837 by (intro_classes, simp add: complex_number_of_def) |
837 by (intro_classes, simp add: complex_number_of_def) |
838 |
838 |