| author | wenzelm |
| Sat, 12 Jun 2021 18:22:07 +0200 | |
| changeset 60298 | 09106b85d3b4 |
| parent 59852 | ea7e6679080e |
| permissions | -rw-r--r-- |
| neuper@52146 | 1 |
theory Thy_2 imports Thy_1 begin |
| neuper@48809 | 2 |
|
| wneuper@59472 | 3 |
ML \<open>val test_list_rls = |
| walther@59852 | 4 |
Rule_Set.append_rules "test_list_rls" Rule_Set.empty |
| wenzelm@60298 | 5 |
[\<^rule_thm>\<open>refl\<close>, \<^rule_thm>\<open>subst\<close>]\<close> |
| neuper@52139 | 6 |
|
| wneuper@59472 | 7 |
setup \<open>Test_KEStore_Elems.add_rlss |
| neuper@52146 | 8 |
[("test_list_rls", (Context.theory_name @{theory}, (*already added in Thy_1.thy*)
|
| wneuper@59472 | 9 |
test_list_rls))]\<close> |
| neuper@52139 | 10 |
|
| wneuper@59472 | 11 |
ML \<open>(*test_ruleset' := overwritelthy @{theory} (! test_ruleset',
|
| neuper@52156 | 12 |
[("test_list_rls", test_list_rls)])*)
|
| wneuper@59472 | 13 |
\<close> |
| neuper@48809 | 14 |
|
| neuper@48794 | 15 |
end |