1605 append_rls "e_rls" e_rls [(*for preds in where_*) |
1605 append_rls "e_rls" e_rls [(*for preds in where_*) |
1606 Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
1606 Calc ("Poly.is'_polyexp", eval_is_polyexp "")], |
1607 SOME "Simplify t_t", |
1607 SOME "Simplify t_t", |
1608 [["simplification","for_polynomials"]])); |
1608 [["simplification","for_polynomials"]])); |
1609 *} |
1609 *} |
1610 setup {* KEStore_Elems.store_pbts |
1610 setup {* KEStore_Elems.add_pbts |
1611 [(prep_pbt thy "pbl_simp_poly" [] e_pblID |
1611 [(prep_pbt thy "pbl_simp_poly" [] e_pblID |
1612 (["polynomial","simplification"], |
1612 (["polynomial","simplification"], |
1613 [("#Given" ,["Term t_t"]), |
1613 [("#Given" ,["Term t_t"]), |
1614 ("#Where" ,["t_t is_polyexp"]), |
1614 ("#Where" ,["t_t is_polyexp"]), |
1615 ("#Find" ,["normalform n_n"])], |
1615 ("#Find" ,["normalform n_n"])], |