equal
deleted
inserted
replaced
70 "(-6) + (-5 * x + (-15 * x ^^^ 2))";*) |
70 "(-6) + (-5 * x + (-15 * x ^^^ 2))";*) |
71 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
71 if term2str t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
72 else raise error "termorder.sml diff.behav ord_make_polynomial_in #14"; |
72 else raise error "termorder.sml diff.behav ord_make_polynomial_in #14"; |
73 |
73 |
74 val SOME (t',_) = |
74 val SOME (t',_) = |
75 rewrite_set_inst "Isac.thy"false [("bdv","x")] "make_polynomial_in" ppp'; |
75 rewrite_set_inst "Isac"false [("bdv","x")] "make_polynomial_in" ppp'; |
76 (*MG 2003... |
76 (*MG 2003... |
77 "(-6) + (-5 * x + (-15) * x ^^^ 2)";*) |
77 "(-6) + (-5 * x + (-15) * x ^^^ 2)";*) |
78 if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
78 if t' = "-6 + -5 * x + -15 * x ^^^ 2 + 0" then () |
79 else raise error "termorder.sml diff.behav ord_make_polynomial_in #15"; |
79 else raise error "termorder.sml diff.behav ord_make_polynomial_in #15"; |
80 |
80 |