| author | wenzelm |
| Sat, 12 Jun 2021 18:22:07 +0200 | |
| changeset 60298 | 09106b85d3b4 |
| parent 59852 | ea7e6679080e |
| permissions | -rw-r--r-- |
1 theory Thy_2b imports Thy_1 begin
3 ML \<open>val test_list_rls =
4 Rule_Set.append_rules "test_list_rls" Rule_Set.empty [\<^rule_thm>\<open>False_def\<close>]\<close>
6 setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory},
7 test_list_rls))]\<close>
8 ML \<open>(*test_ruleset' := overwritelthy @{theory} (! test_ruleset',
9 [("test_list_rls", test_list_rls)])*)
10 \<close>
12 end