equal
deleted
inserted
replaced
691 "-------- ord_make_polynomial ------------------------------------------------------------------"; |
691 "-------- ord_make_polynomial ------------------------------------------------------------------"; |
692 "-------- ord_make_polynomial ------------------------------------------------------------------"; |
692 "-------- ord_make_polynomial ------------------------------------------------------------------"; |
693 val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)"; |
693 val t1 = TermC.parse_test @{context} "2 * b + (3 * a + 3 * b)"; |
694 val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b"; |
694 val t2 = TermC.parse_test @{context} "(3 * a + 3 * b) + 2 * b"; |
695 |
695 |
696 if ord_make_polynomial true @{theory} [] (t1, t2) then () |
696 if ord_make_polynomial true @{context} [] (t1, t2) then () |
697 else error "poly.sml: diff.behav. in ord_make_polynomial"; |
697 else error "poly.sml: diff.behav. in ord_make_polynomial"; |
698 (*SO: WHY IS THERE NO REWRITING ...*) |
698 (*SO: WHY IS THERE NO REWRITING ...*) |
699 |
699 |
700 val term = TermC.parse_test @{context} "2*b + (3*a + 3*b)"; |
700 val term = TermC.parse_test @{context} "2*b + (3*a + 3*b)"; |
701 (*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term; |
701 (*+++*)val NONE = rewrite_set_ (Proof_Context.init_global @{theory "Isac_Knowledge"}) false order_add_mult term; |