equal
deleted
inserted
replaced
1 theory Thy_2b imports Thy_1 begin |
1 theory Thy_2b imports Thy_1 begin |
2 |
2 |
3 ML {* val test_list_rls = |
3 ML {* val test_list_rls = |
4 append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})] *} |
4 append_rls "test_list_rls" e_rls [Thm ("False_def", @{thm False_def})] *} |
5 |
5 |
6 setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, |
6 setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, |
7 test_list_rls))] *} |
7 test_list_rls))] *} |
8 ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', |
8 ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', |
9 [("test_list_rls", test_list_rls)])*) |
9 [("test_list_rls", test_list_rls)])*) |
10 *} |
10 *} |
11 |
11 |