equal
deleted
inserted
replaced
379 (*if there is ... |
379 (*if there is ... |
380 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt; |
380 > val NoMatch' {Given=gi, Where=wh, Find=fi,...} = match_pbl fmz pbt; |
381 ... then trace_rewrite:*) |
381 ... then trace_rewrite:*) |
382 |
382 |
383 "-----2 ---"; |
383 "-----2 ---"; |
384 trace_rewrite := true; |
384 trace_rewrite := false; |
385 match_pbl fmz pbt; |
385 match_pbl fmz pbt; |
386 trace_rewrite := false; |
386 trace_rewrite := false; |
387 (*... if there is no rewrite, then there is something wrong with prls*) |
387 (*... if there is no rewrite, then there is something wrong with prls*) |
388 |
388 |
389 "-----3 ---"; |
389 "-----3 ---"; |
390 print_depth 7; |
390 print_depth 7; |
391 val prls = (#prls o get_pbt) ["polynomial","simplification"]; |
391 val prls = (#prls o get_pbt) ["polynomial","simplification"]; |
392 print_depth 3; |
392 print_depth 3; |
393 val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp"; |
393 val t = str2term "((5*x^^^2 + 3) * (2*x^^^7 + 3) - (3*x^^^5 + 8) * (6*x^^^4 - 1)) is_polyexp"; |