equal
deleted
inserted
replaced
1428 if ord_make_polynomial true thy [] (t1, t2) then () |
1428 if ord_make_polynomial true thy [] (t1, t2) then () |
1429 else error "poly.sml: diff.behav. in ord_make_polynomial"; |
1429 else error "poly.sml: diff.behav. in ord_make_polynomial"; |
1430 (*SO: WHY IS THERE NO REWRITING ...*) |
1430 (*SO: WHY IS THERE NO REWRITING ...*) |
1431 |
1431 |
1432 val term = TermC.str2term "2*b + (3*a + 3*b)"; |
1432 val term = TermC.str2term "2*b + (3*a + 3*b)"; |
1433 (*+++*)val SOME (t', []) = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term; |
1433 (*+++*)val NONE = rewrite_set_ @{theory "Isac_Knowledge"} false order_add_mult term; |
1434 (*+++*)if UnparseC.term t' = "a * 3 + (b * 2 + b * 3)" then () else error "no rewriting ?!?"; |
1434 (* |
1435 (* before dropping ThmC.numerals_to_Free this was |
1435 WHY IS THERE NO REWRITING ?!? |
1436 val NONE = rewrite_set_ @ {theory "Isac_Knowledge"} false order_add_mult term; |
1436 most likely reason: Poly.thy and Rationa.thy do AC rewriting in ML, |
1437 SO: WHY IS THERE NO REWRITING ?!? |
1437 while order_add_mult uses isac's rewriter -- and this is used rarely! |
1438 *) |
1438 *) |
1439 |
1439 |