author | wenzelm |
Sat, 12 Jun 2021 18:22:07 +0200 | |
changeset 60298 | 09106b85d3b4 |
parent 59878 | 3163e63a5111 |
permissions | -rw-r--r-- |
neuper@52146 | 1 |
theory Thy_3 imports Thy_2 Thy_2b begin |
neuper@48809 | 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>not_def\<close>]\<close> |
neuper@52139 | 5 |
|
wneuper@59472 | 6 |
setup \<open>Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*) |
wneuper@59472 | 7 |
[("test_list_rls", (Context.theory_name @{theory}, test_list_rls))]\<close> |
neuper@52139 | 8 |
|
wneuper@59472 | 9 |
ML \<open> |
s1210629013@55359 | 10 |
if length (Test_KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*) |
neuper@52126 | 11 |
then () else error "rls identified by string-identifier, not by theory: changed" |
neuper@52139 | 12 |
|
neuper@52156 | 13 |
(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", |
walther@59878 | 14 |
Rule_Set.append_rules "test_list_rls" test_list_rls [Eval ("test_function", e_evalfn)])])*) |
neuper@52126 | 15 |
; |
s1210629013@55359 | 16 |
(*if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') |
s1210629013@55359 | 17 |
then () else error "Test_KEStore_Elems.get_rlss = test_ruleset': changed"*) |
neuper@52139 | 18 |
; |
walther@59851 | 19 |
val SOME (_, Rule_Set.Repeat {rules, ...}) = |
s1210629013@55359 | 20 |
AList.lookup op= (Test_KEStore_Elems.get_rlss @{theory}) "test_list_rls" |
neuper@52139 | 21 |
; |
neuper@52139 | 22 |
case rules of |
wneuper@59417 | 23 |
[Rule.Thm ("not_def", _)] => () |
neuper@52139 | 24 |
| _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore" |
walther@59867 | 25 |
(* merge rules of rls with the same Rule_Set.id must be done one level higher: |
s1210629013@55359 | 26 |
Test_KEStore_Elems.add_rlss does *add* or *overwrite* *) |
wneuper@59472 | 27 |
\<close> |
neuper@48809 | 28 |
|
neuper@48794 | 29 |
end |