133 Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}), |
133 Thm ("sqrt_conv_bdv", num_str @{thm sqrt_conv_bdv}), |
134 Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}), |
134 Thm ("sqrt_conv_bdv_n", num_str @{thm sqrt_conv_bdv_n}), |
135 Thm ("sqrt_conv", num_str @{thm sqrt_conv}), |
135 Thm ("sqrt_conv", num_str @{thm sqrt_conv}), |
136 Thm ("root_conv", num_str @{thm root_conv}), |
136 Thm ("root_conv", num_str @{thm root_conv}), |
137 Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}), |
137 Thm ("realpow_pow_bdv", num_str @{thm realpow_pow_bdv}), |
138 Calc ("op *", eval_binop "#mult_"), |
138 Calc ("Groups.times_class.times", eval_binop "#mult_"), |
139 Thm ("rat_mult",num_str @{thm rat_mult}), |
139 Thm ("rat_mult",num_str @{thm rat_mult}), |
140 (*a / b * (c / d) = a * c / (b * d)*) |
140 (*a / b * (c / d) = a * c / (b * d)*) |
141 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
141 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
142 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
142 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
143 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}) |
143 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}) |
165 (*a / b * (c / d) = a * c / (b * d)*) |
165 (*a / b * (c / d) = a * c / (b * d)*) |
166 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
166 Thm ("times_divide_eq_right",num_str @{thm times_divide_eq_right}), |
167 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
167 (*?x * (?y / ?z) = ?x * ?y / ?z*) |
168 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
168 Thm ("times_divide_eq_left",num_str @{thm times_divide_eq_left}), |
169 (*?y / ?z * ?x = ?y * ?x / ?z*) |
169 (*?y / ?z * ?x = ?y * ?x / ?z*) |
170 Calc ("op *", eval_binop "#mult_") |
170 Calc ("Groups.times_class.times", eval_binop "#mult_") |
171 ], |
171 ], |
172 scr = EmptyScr}; |
172 scr = EmptyScr}; |
173 |
173 |
174 (*..*) |
174 (*..*) |
175 val srls_diff = |
175 val srls_diff = |