216 | eval_rhs _ _ _ _ = NONE; |
216 | eval_rhs _ _ _ _ = NONE; |
217 |
217 |
218 |
218 |
219 (*for evaluating scripts*) |
219 (*for evaluating scripts*) |
220 |
220 |
221 val list_rls = append_rls "list_rls" list_rls |
221 val list_rls = append_rls "list_rls" list_rls [Calc ("Tools.rhs", eval_rhs "")]; |
222 [Calc ("Tools.rhs",eval_rhs "")]; |
222 |
223 ruleset' := overwritelthy @{theory} (!ruleset', |
223 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]); |
224 [("list_rls",list_rls) |
|
225 ]); |
|
226 *} |
224 *} |
227 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
225 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
228 ML {* |
226 ML {* |
229 calclist':= overwritel (!calclist', |
227 calclist':= overwritel (!calclist', |
230 [("matches",("Tools.matches",eval_matches "#matches_")), |
228 [("matches",("Tools.matches",eval_matches "#matches_")), |
231 ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")), |
229 ("matchsub",("Tools.matchsub",eval_matchsub "#matchsub_")), |
232 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")), |
230 ("Vars" ,("Tools.Vars" ,eval_var "#Vars_")), |
233 ("lhs" ,("Tools.lhs" ,eval_lhs "")), |
231 ("lhs" ,("Tools.lhs" ,eval_lhs "")), |
234 ("rhs" ,("Tools.rhs" ,eval_rhs "")) |
232 ("rhs" ,("Tools.rhs" ,eval_rhs "")) |
235 ]); |
233 ]); |
236 |
|
237 *} |
234 *} |
|
235 |
238 end |
236 end |