equal
deleted
inserted
replaced
894 ], |
894 ], |
895 append_rls "e_rls" e_rls [(*for preds in where_*)], |
895 append_rls "e_rls" e_rls [(*for preds in where_*)], |
896 SOME "Simplify t_t", |
896 SOME "Simplify t_t", |
897 [["simplification","of_rationals"]])); |
897 [["simplification","of_rationals"]])); |
898 *} |
898 *} |
899 setup {* KEStore_Elems.store_pbts |
899 setup {* KEStore_Elems.add_pbts |
900 [(prep_pbt thy "pbl_simp_rat" [] e_pblID |
900 [(prep_pbt thy "pbl_simp_rat" [] e_pblID |
901 (["rational","simplification"], |
901 (["rational","simplification"], |
902 [("#Given" ,["Term t_t"]), |
902 [("#Given" ,["Term t_t"]), |
903 ("#Where" ,["t_t is_ratpolyexp"]), |
903 ("#Where" ,["t_t is_ratpolyexp"]), |
904 ("#Find" ,["normalform n_n"])], |
904 ("#Find" ,["normalform n_n"])], |