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