equal
deleted
inserted
replaced
63 by transfer (rule mult_scaleR_right) |
63 by transfer (rule mult_scaleR_right) |
64 qed |
64 qed |
65 |
65 |
66 instance star :: (real_algebra_1) real_algebra_1 .. |
66 instance star :: (real_algebra_1) real_algebra_1 .. |
67 |
67 |
|
68 instance star :: (real_div_algebra) real_div_algebra .. |
|
69 |
|
70 instance star :: (real_field) real_field .. |
|
71 |
68 lemma star_of_real_def [transfer_unfold]: "of_real r \<equiv> star_of (of_real r)" |
72 lemma star_of_real_def [transfer_unfold]: "of_real r \<equiv> star_of (of_real r)" |
69 by (rule eq_reflection, unfold of_real_def, transfer, rule refl) |
73 by (rule eq_reflection, unfold of_real_def, transfer, rule refl) |
70 |
74 |
71 lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" |
75 lemma star_of_of_real [simp]: "star_of (of_real r) = of_real r" |
72 by transfer (rule refl) |
76 by transfer (rule refl) |