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