equal
deleted
inserted
replaced
317 else error "polyminus.sml: fasse_zusammen finished"; |
317 else error "polyminus.sml: fasse_zusammen finished"; |
318 |
318 |
319 "----------- build verschoenere ----------------------------------"; |
319 "----------- build verschoenere ----------------------------------"; |
320 "----------- build verschoenere ----------------------------------"; |
320 "----------- build verschoenere ----------------------------------"; |
321 "----------- build verschoenere ----------------------------------"; |
321 "----------- build verschoenere ----------------------------------"; |
322 val t = TermC.str2term "3 + -2 * e + 2 * f + 2 * g"; |
322 val t = TermC.str2term "3 + - 2 * e + 2 * f + 2 * g"; |
323 val SOME (t,_) = rewrite_set_ thy false verschoenere t; |
323 val SOME (t,_) = rewrite_set_ thy false verschoenere t; |
324 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then () |
324 if UnparseC.term t = "3 - 2 * e + 2 * f + 2 * g" then () |
325 else error "polyminus.sml: verschoenere 3 + -2 * e ..."; |
325 else error "polyminus.sml: verschoenere 3 + - 2 * e ..."; |
326 |
326 |
327 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) |
327 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) |
328 Rewrite.trace_on:=false; |
328 Rewrite.trace_on:=false; |
329 |
329 |
330 "----------- met simplification for_polynomials with_minus -------"; |
330 "----------- met simplification for_polynomials with_minus -------"; |