1 theory Thy_3 imports Thy_2 Thy_2b begin |
1 theory Thy_3 imports Thy_2 Thy_2b begin |
2 |
2 |
3 ML {* val test_list_rls = |
3 ML {* val test_list_rls = |
4 append_rls "test_list_rls" e_rls [Thm ("not_def", @{thm not_def})] *} |
4 append_rls "test_list_rls" e_rls [Thm ("not_def", @{thm not_def})] *} |
5 |
5 |
6 setup {* KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*) |
6 setup {* Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*) |
7 [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *} |
7 [("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *} |
8 |
8 |
9 ML {* |
9 ML {* |
10 if length (KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*) |
10 if length (Test_KEStore_Elems.get_rlss @{theory}) = 1 (*stored in 3 different theories*) |
11 then () else error "rls identified by string-identifier, not by theory: changed" |
11 then () else error "rls identified by string-identifier, not by theory: changed" |
12 |
12 |
13 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", |
13 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", |
14 append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])*) |
14 append_rls "test_list_rls" test_list_rls [Calc ("test_function", e_evalfn)])])*) |
15 ; |
15 ; |
16 (*if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') |
16 (*if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') |
17 then () else error "KEStore_Elems.get_rlss = test_ruleset': changed"*) |
17 then () else error "Test_KEStore_Elems.get_rlss = test_ruleset': changed"*) |
18 ; |
18 ; |
19 val SOME (_, Rls {rules, ...}) = |
19 val SOME (_, Rls {rules, ...}) = |
20 AList.lookup op= (KEStore_Elems.get_rlss @{theory}) "test_list_rls" |
20 AList.lookup op= (Test_KEStore_Elems.get_rlss @{theory}) "test_list_rls" |
21 ; |
21 ; |
22 case rules of |
22 case rules of |
23 [Thm ("not_def", _)] => () |
23 [Thm ("not_def", _)] => () |
24 | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore" |
24 | _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore" |
25 (* merge rules of rls with the same identifier rls' must be done one level higher: |
25 (* merge rules of rls with the same identifier rls' must be done one level higher: |
26 KEStore_Elems.add_rlss does *add* or *overwrite* *) |
26 Test_KEStore_Elems.add_rlss does *add* or *overwrite* *) |
27 *} |
27 *} |
28 |
28 |
29 end |
29 end |