equal
deleted
inserted
replaced
714 list_rls); |
714 list_rls); |
715 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]); |
715 ruleset' := overwritelthy @{theory} (!ruleset', [("list_rls", list_rls)]); |
716 *} |
716 *} |
717 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
717 setup {* KEStore_Elems.add_rlss [("list_rls", (Context.theory_name @{theory}, list_rls))] *} |
718 |
718 |
|
719 ML {* |
|
720 (* BEFORE EVALUATING val eval_rls = IN DiffApp (!!!), |
|
721 AFTER ./bin/isabelle jedit -l HOL src/Tools/isac/Knowledge/DiffApp.thy & |
|
722 HERE IS ME_Isa: 'eval_rls' not in system ...*) |
|
723 assoc_rls "eval_rls" (* = Rls {id = "Atools_erls", scr = ... AFTER EVALUATING*) |
|
724 *} |
719 end |
725 end |