896 by (intro_classes; transfer) (fact abs_eq_mult) |
896 by (intro_classes; transfer) (fact abs_eq_mult) |
897 |
897 |
898 instance star :: (abs_if) abs_if |
898 instance star :: (abs_if) abs_if |
899 by (intro_classes; transfer) (fact abs_if) |
899 by (intro_classes; transfer) (fact abs_if) |
900 |
900 |
901 instance star :: (sgn_if) sgn_if |
|
902 by (intro_classes; transfer) (fact sgn_if) |
|
903 |
|
904 instance star :: (linordered_ring_strict) linordered_ring_strict .. |
901 instance star :: (linordered_ring_strict) linordered_ring_strict .. |
905 instance star :: (ordered_comm_ring) ordered_comm_ring .. |
902 instance star :: (ordered_comm_ring) ordered_comm_ring .. |
906 |
903 |
907 instance star :: (linordered_semidom) linordered_semidom |
904 instance star :: (linordered_semidom) linordered_semidom |
908 apply intro_classes |
905 by (intro_classes; transfer) (fact zero_less_one le_add_diff_inverse2)+ |
909 apply(transfer, fact zero_less_one) |
906 |
910 apply(transfer, fact le_add_diff_inverse2) |
907 instance star :: (linordered_idom) linordered_idom |
911 done |
908 by (intro_classes; transfer) (fact sgn_if) |
912 |
909 |
913 instance star :: (linordered_idom) linordered_idom .. |
|
914 instance star :: (linordered_field) linordered_field .. |
910 instance star :: (linordered_field) linordered_field .. |
915 |
911 |
916 subsection \<open>Power\<close> |
912 subsection \<open>Power\<close> |
917 |
913 |
918 lemma star_power_def [transfer_unfold]: |
914 lemma star_power_def [transfer_unfold]: |