equal
deleted
inserted
replaced
1 theory Thy_2b imports Thy_1 begin |
1 theory Thy_2b 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 [Rule.Thm ("False_def", @{thm False_def})]\<close> |
4 Rule_Set.append_rules "test_list_rls" Rule_Set.empty [\<^rule_thm>\<open>False_def\<close>]\<close> |
5 |
5 |
6 setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, |
6 setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, |
7 test_list_rls))]\<close> |
7 test_list_rls))]\<close> |
8 ML \<open>(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', |
8 ML \<open>(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', |
9 [("test_list_rls", test_list_rls)])*) |
9 [("test_list_rls", test_list_rls)])*) |