565 \a - 2 * q + 3 * (a - 2 * q)) = True", _) => () |
565 \a - 2 * q + 3 * (a - 2 * q)) = True", _) => () |
566 | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A"; |
566 | _ => error "polyminus.sml matchsub (?a * (?b - ?c)...A"; |
567 |
567 |
568 "--- does the respective prls rewrite ?"; |
568 "--- does the respective prls rewrite ?"; |
569 val prls = append_rls "prls_pbl_vereinf_poly" e_rls |
569 val prls = append_rls "prls_pbl_vereinf_poly" e_rls |
570 [Calc ("Poly.is'_polyexp", eval_is_polyexp ""), |
570 [Num_Calc ("Poly.is'_polyexp", eval_is_polyexp ""), |
571 Calc ("Prog_Expr.matchsub", eval_matchsub ""), |
571 Num_Calc ("Prog_Expr.matchsub", eval_matchsub ""), |
572 Thm ("or_true",@{thm or_true}), |
572 Thm ("or_true",@{thm or_true}), |
573 (*"(?a | True) = True"*) |
573 (*"(?a | True) = True"*) |
574 Thm ("or_false",@{thm or_false}), |
574 Thm ("or_false",@{thm or_false}), |
575 (*"(?a | False) = ?a"*) |
575 (*"(?a | False) = ?a"*) |
576 Thm ("not_true",num_str @{thm not_true}), |
576 Thm ("not_true",num_str @{thm not_true}), |