130 Thm ("root_conv", num_str root_conv), |
130 Thm ("root_conv", num_str root_conv), |
131 Thm ("realpow_pow_bdv", num_str realpow_pow_bdv), |
131 Thm ("realpow_pow_bdv", num_str realpow_pow_bdv), |
132 Calc ("op *", eval_binop "#mult_"), |
132 Calc ("op *", eval_binop "#mult_"), |
133 Thm ("rat_mult",num_str rat_mult), |
133 Thm ("rat_mult",num_str rat_mult), |
134 (*a / b * (c / d) = a * c / (b * d)*) |
134 (*a / b * (c / d) = a * c / (b * d)*) |
135 Thm ("real_times_divide1_eq",num_str real_times_divide1_eq), |
135 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
136 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
136 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
137 Thm ("real_times_divide2_eq",num_str real_times_divide2_eq) |
137 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}) |
138 (*?y / ?z * ?x = ?y * ?x / ?z*) |
138 (*?y / ?z * ?x = ?y * ?x / ?z*) |
139 (* |
139 (* |
140 Thm ("", num_str ),*) |
140 Thm ("", num_str ),*) |
141 ], |
141 ], |
142 scr = EmptyScr}; |
142 scr = EmptyScr}; |
156 Thm ("sym_real_mult_minus1", |
156 Thm ("sym_real_mult_minus1", |
157 num_str (real_mult_minus1 RS sym)), |
157 num_str (real_mult_minus1 RS sym)), |
158 (*- ?z = "-1 * ?z"*) |
158 (*- ?z = "-1 * ?z"*) |
159 Thm ("rat_mult",num_str rat_mult), |
159 Thm ("rat_mult",num_str rat_mult), |
160 (*a / b * (c / d) = a * c / (b * d)*) |
160 (*a / b * (c / d) = a * c / (b * d)*) |
161 Thm ("real_times_divide1_eq",num_str real_times_divide1_eq), |
161 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
162 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
162 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
163 Thm ("real_times_divide2_eq",num_str real_times_divide2_eq), |
163 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
164 (*?y / ?z * ?x = ?y * ?x / ?z*) |
164 (*?y / ?z * ?x = ?y * ?x / ?z*) |
165 Calc ("op *", eval_binop "#mult_") |
165 Calc ("op *", eval_binop "#mult_") |
166 ], |
166 ], |
167 scr = EmptyScr}; |
167 scr = EmptyScr}; |
168 |
168 |