544 ]; |
544 ]; |
545 |
545 |
546 ruleset' := overwritelthy thy (!ruleset', |
546 ruleset' := overwritelthy thy (!ruleset', |
547 [("list_rls",list_rls) |
547 [("list_rls",list_rls) |
548 ]); |
548 ]); |
|
549 *} |
|
550 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
|
551 ML {* |
549 |
552 |
550 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*) |
553 (*TODO.WN0509 reduce ids: tless_true = e_rew_ord' = e_rew_ord = dummy_ord*) |
551 val tless_true = dummy_ord; |
554 val tless_true = dummy_ord; |
552 rew_ord' := overwritel (!rew_ord', |
555 rew_ord' := overwritel (!rew_ord', |
553 [("tless_true", tless_true), |
556 [("tless_true", tless_true), |
640 Calc ("Atools.occurs'_in", |
643 Calc ("Atools.occurs'_in", |
641 eval_occurs_in "#occurs_in"), |
644 eval_occurs_in "#occurs_in"), |
642 Calc ("Tools.matches",eval_matches "#matches") |
645 Calc ("Tools.matches",eval_matches "#matches") |
643 ] (*i.A. zu viele rules*) |
646 ] (*i.A. zu viele rules*) |
644 );*) |
647 );*) |
645 (* val atools_erls = prep_rls( |
648 (* val atools_erls = prep_rls( (*outcommented*) |
646 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), |
649 Rls {id="atools_erls",preconds = [], rew_ord = ("termlessI",termlessI), |
647 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
650 erls = e_rls, srls = Erls, calc = [], errpatts = [], |
648 rules = [Thm ("refl",num_str @{thm refl}), |
651 rules = [Thm ("refl",num_str @{thm refl}), |
649 Thm ("order_refl",num_str @{thm order_refl}), |
652 Thm ("order_refl",num_str @{thm order_refl}), |
650 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}), |
653 Thm ("radd_left_cancel_le",num_str @{thm radd_left_cancel_le}), |
665 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
668 Calc ("Atools.occurs'_in",eval_occurs_in ""), |
666 Calc ("Tools.matches",eval_matches "") |
669 Calc ("Tools.matches",eval_matches "") |
667 ], |
670 ], |
668 scr = Prog ((term_of o the o (parse @{theory})) "empty_script") |
671 scr = Prog ((term_of o the o (parse @{theory})) "empty_script") |
669 }:rls); |
672 }:rls); |
670 ruleset' := overwritelth @{theory} |
673 ruleset' := overwritelth @{theory} (*outcommented*) |
671 (!ruleset', |
674 (!ruleset', |
672 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*) |
675 [("atools_erls",atools_erls)(*FIXXXME:del with rls.rls'*) |
673 ]); |
676 ]); |
674 *) |
677 *) |
675 "******* Atools.ML end *******"; |
678 "******* Atools.ML end *******"; |
709 srls = Erls, calc = [], errpatts = [], |
712 srls = Erls, calc = [], errpatts = [], |
710 rules = [], scr = EmptyScr}) |
713 rules = [], scr = EmptyScr}) |
711 list_rls); |
714 list_rls); |
712 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]); |
715 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]); |
713 *} |
716 *} |
|
717 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
714 |
718 |
715 end |
719 end |