equal
deleted
inserted
replaced
1 theory Thy_2 imports Thy_1 begin |
1 theory Thy_2 imports Thy_1 begin |
2 |
2 |
3 ML \<open>val test_list_rls = |
3 ML \<open>val test_list_rls = |
4 Rule_Set.append_rules "test_list_rls" Rule_Set.empty |
4 Rule_Set.append_rules "test_list_rls" Rule_Set.empty |
5 [Rule.Thm ("refl", @{thm refl}), Rule.Thm ("subst", @{thm subst})]\<close> |
5 [\<^rule_thm>\<open>refl\<close>, \<^rule_thm>\<open>subst\<close>]\<close> |
6 |
6 |
7 setup \<open>Test_KEStore_Elems.add_rlss |
7 setup \<open>Test_KEStore_Elems.add_rlss |
8 [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*) |
8 [("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*) |
9 test_list_rls))]\<close> |
9 test_list_rls))]\<close> |
10 |
10 |