238 erls = Erls, srls = Erls, calc = [], errpatts = [], |
238 erls = Erls, srls = Erls, calc = [], errpatts = [], |
239 rules = [Rls_ diff_rules, Rls_ norm_Poly ], |
239 rules = [Rls_ diff_rules, Rls_ norm_Poly ], |
240 scr = EmptyScr}; |
240 scr = EmptyScr}; |
241 *} |
241 *} |
242 setup {* KEStore_Elems.add_rlss |
242 setup {* KEStore_Elems.add_rlss |
243 [("erls_diff", (Context.theory_name @{theory}, prep_rls erls_diff)), |
243 [("erls_diff", (Context.theory_name @{theory}, prep_rls' erls_diff)), |
244 ("diff_rules", (Context.theory_name @{theory}, prep_rls diff_rules)), |
244 ("diff_rules", (Context.theory_name @{theory}, prep_rls' diff_rules)), |
245 ("norm_diff", (Context.theory_name @{theory}, prep_rls norm_diff)), |
245 ("norm_diff", (Context.theory_name @{theory}, prep_rls' norm_diff)), |
246 ("diff_conv", (Context.theory_name @{theory}, prep_rls diff_conv)), |
246 ("diff_conv", (Context.theory_name @{theory}, prep_rls' diff_conv)), |
247 ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls diff_sym_conv))] *} |
247 ("diff_sym_conv", (Context.theory_name @{theory}, prep_rls' diff_sym_conv))] *} |
248 |
248 |
249 (** problem types **) |
249 (** problem types **) |
250 setup {* KEStore_Elems.add_pbts |
250 setup {* KEStore_Elems.add_pbts |
251 [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])), |
251 [(prep_pbt thy "pbl_fun" [] e_pblID (["function"], [], e_rls, NONE, [])), |
252 (prep_pbt thy "pbl_fun_deriv" [] e_pblID |
252 (prep_pbt thy "pbl_fun_deriv" [] e_pblID |