equal
deleted
inserted
replaced
255 case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of |
255 case eval_kleiner 0 0 (TermC.str2term "(3*a*b) kleiner c") 0 of |
256 SOME ("3 * a * b kleiner c = True", _) => () |
256 SOME ("3 * a * b kleiner c = True", _) => () |
257 | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; |
257 | _ => error "polyminus.sml: 3 * a * b kleiner b = True"; |
258 |
258 |
259 "======= compare tausche_plus with real_num_collect"; |
259 "======= compare tausche_plus with real_num_collect"; |
260 val od = dummy_ord; |
260 val od = Rewrite_Ord.function_empty; |
261 |
261 |
262 val erls = erls_ordne_alphabetisch; |
262 val erls = erls_ordne_alphabetisch; |
263 val t = TermC.str2term "b + a"; |
263 val t = TermC.str2term "b + a"; |
264 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t; |
264 val SOME (t,_) = rewrite_ ctxt od erls false @{thm tausche_plus} t; UnparseC.term t; |
265 if UnparseC.term t = "a + b" then () |
265 if UnparseC.term t = "a + b" then () |
524 "----- 2 \<up> "; |
524 "----- 2 \<up> "; |
525 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) |
525 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*) |
526 val erls = erls_ordne_alphabetisch; |
526 val erls = erls_ordne_alphabetisch; |
527 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
527 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
528 val SOME (t',_) = |
528 val SOME (t',_) = |
529 rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus} t; |
529 rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus} t; |
530 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g"; |
530 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e + (- 4 + 6) * f - 8 * g + 10 * g"; |
531 |
531 |
532 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
532 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
533 val NONE = |
533 val NONE = |
534 rewrite_ ctxt e_rew_ord erls false @{thm tausche_minus_plus} t; |
534 rewrite_ ctxt Rewrite_Ord.function_empty erls false @{thm tausche_minus_plus} t; |
535 |
535 |
536 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
536 val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g"; |
537 val SOME (t',_) = |
537 val SOME (t',_) = |
538 rewrite_set_ ctxt false ordne_alphabetisch t; |
538 rewrite_set_ ctxt false ordne_alphabetisch t; |
539 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f"; |
539 UnparseC.term t'; "- 9 + 12 + 5 * e - 7 * e - 8 * g + 10 * g + (- 4 + 6) * f"; |