|
neuper@52146
|
1 |
theory Thy_3 imports Thy_2 Thy_2b begin
|
|
neuper@48809
|
2 |
|
|
neuper@52139
|
3 |
ML {* val test_list_rls =
|
|
neuper@52139
|
4 |
append_rls "test_list_rls" e_rls [Thm ("not_def", @{thm not_def})] *}
|
|
neuper@52139
|
5 |
|
|
s1210629013@55359
|
6 |
setup {* Test_KEStore_Elems.add_rlss (*already added in Thy_1.thy and Thy_2.thy*)
|
|
neuper@52139
|
7 |
[("test_list_rls", (Context.theory_name @{theory}, test_list_rls))] *}
|
|
neuper@52139
|
8 |
|
|
neuper@52126
|
9 |
ML {*
|
|
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",
|
|
neuper@52156
|
14 |
append_rls "test_list_rls" test_list_rls [Calc ("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 |
;
|
|
neuper@52139
|
19 |
val SOME (_, Rls {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
|
|
neuper@52139
|
23 |
[Thm ("not_def", _)] => ()
|
|
neuper@52139
|
24 |
| _ => error "union rls_eq changed: 1st argument is NOT overwritten anymore"
|
|
neuper@52139
|
25 |
(* merge rules of rls with the same identifier rls' must be done one level higher:
|
|
s1210629013@55359
|
26 |
Test_KEStore_Elems.add_rlss does *add* or *overwrite* *)
|
|
neuper@52126
|
27 |
*}
|
|
neuper@48809
|
28 |
|
|
neuper@48794
|
29 |
end
|