equal
deleted
inserted
replaced
664 |
664 |
665 "----- go into details, if it seems not to work -----"; |
665 "----- go into details, if it seems not to work -----"; |
666 "--- does the predicate evaluate correctly ?"; |
666 "--- does the predicate evaluate correctly ?"; |
667 val t = TermC.str2term |
667 val t = TermC.str2term |
668 "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))"; |
668 "matchsub (?a * (?b - ?c)) (8 * (a - q) + a - 2 * q + 3 * (a - 2 * (q::real)))"; |
669 val ma = eval_matchsub "" "Prog_Expr.matchsub" t thy; |
669 val ma = eval_matchsub "" "Prog_Expr.matchsub" t ctxt; |
670 case ma of |
670 case ma of |
671 SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \ |
671 SOME ("matchsub (?a * (?b - ?c)) (8 * (a - q) + \ |
672 \a - 2 * q + 3 * (a - 2 * q)) = True", _) => () |
672 \a - 2 * q + 3 * (a - 2 * q)) = True", _) => () |
673 | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A"; |
673 | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A"; |
674 |
674 |