equal
deleted
inserted
replaced
1 theory Thy_2 imports Thy_1 begin |
1 theory Thy_2 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 ("refl", @{thm refl}), Thm ("subst", @{thm subst})] *} |
4 append_rls "test_list_rls" e_rls [Thm ("refl", @{thm refl}), Thm ("subst", @{thm subst})] *} |
5 |
5 |
6 setup {* KEStore_Elems.add_rlss |
6 setup {* Test_KEStore_Elems.add_rlss |
7 [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*) |
7 [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*) |
8 test_list_rls))] *} |
8 test_list_rls))] *} |
9 |
9 |
10 ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', |
10 ML {* (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', |
11 [("test_list_rls", test_list_rls)])*) |
11 [("test_list_rls", test_list_rls)])*) |