1 theory Thy_1 imports Lucas_Interpreter begin |
1 theory Thy_1 imports Lucas_Interpreter begin |
2 |
2 |
3 ML {* |
3 ML {* |
4 (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset') |
4 (* CHECK length (Test_KEStore_Elems.get_rlss @{theory}) = length (! ruleset') |
5 AT THE BOTTOM OF A THEORY:*) |
5 AT THE BOTTOM OF A THEORY:*) |
6 length (KEStore_Elems.get_rlss @{theory}) = 0; |
6 length (Test_KEStore_Elems.get_rlss @{theory}) = 0; |
7 (*length (! test_ruleset') = 1 (* if you have clicked somewhere below *)*) |
7 (*length (! test_ruleset') = 1 (* if you have clicked somewhere below *)*) |
8 *} |
8 *} |
9 setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *} |
9 setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *} |
10 ML {* |
10 ML {* |
11 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)]) |
11 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)]) |
12 ; |
12 ; |
13 if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then () |
13 if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then () |
14 else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*) |
14 else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*) |
15 *} |
15 *} |
16 |
16 |
17 setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *} |
17 setup {* Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *} |
18 |
18 |
19 end |
19 end |