equal
deleted
inserted
replaced
280 if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2"; |
280 if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2"; |
281 |
281 |
282 val t = str2term "2 / sqrt x^^^3"; |
282 val t = str2term "2 / sqrt x^^^3"; |
283 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
283 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
284 if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2"; |
284 if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2"; |
285 (* trace_rewrite := true; |
|
286 trace_rewrite := false; |
|
287 *) |
|
288 val rls = diff_sym_conv; |
285 val rls = diff_sym_conv; |
289 |
286 |
290 val t = str2term "2 * x ^^^ -2"; |
287 val t = str2term "2 * x ^^^ -2"; |
291 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
288 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
292 if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x"; |
289 if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x"; |
298 |
295 |
299 val t = str2term "2 * x ^^^ (-3 / 2)"; |
296 val t = str2term "2 * x ^^^ (-3 / 2)"; |
300 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
297 val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t; |
301 if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x"; |
298 if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x"; |
302 |
299 |
303 |
|
304 (* trace_rewrite:=true; |
|
305 *) |
|
306 (* trace_rewrite:=false; |
|
307 *) |
|
308 (*@@@@*) |
|
309 |
300 |
310 "----------- autoCalculate differentiate_on_R 2/x^2 -----"; |
301 "----------- autoCalculate differentiate_on_R 2/x^2 -----"; |
311 "----------- autoCalculate differentiate_on_R 2/x^2 -----"; |
302 "----------- autoCalculate differentiate_on_R 2/x^2 -----"; |
312 "----------- autoCalculate differentiate_on_R 2/x^2 -----"; |
303 "----------- autoCalculate differentiate_on_R 2/x^2 -----"; |
313 reset_states (); |
304 reset_states (); |
332 "differentiateFor x", "derivative f_f'"], |
323 "differentiateFor x", "derivative f_f'"], |
333 ("Isac_Knowledge", ["derivative_of","function"], |
324 ("Isac_Knowledge", ["derivative_of","function"], |
334 ["diff","differentiate_on_R"]))]; |
325 ["diff","differentiate_on_R"]))]; |
335 Iterator 1; |
326 Iterator 1; |
336 moveActiveRoot 1; |
327 moveActiveRoot 1; |
|
328 autoCalculate 1 CompleteCalc; |
337 (* trace_rewrite := true; |
329 (* trace_rewrite := true; |
338 trace_script := true; |
|
339 *) |
|
340 autoCalculate 1 CompleteCalc; |
|
341 (* trace_rewrite := false; |
|
342 trace_script := false; |
330 trace_script := false; |
343 *) |
331 *) |
344 val ((pt,p),_) = get_calc 1; show_pt pt; |
332 val ((pt,p),_) = get_calc 1; show_pt pt; |
345 |
333 |
346 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = |
334 if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = |