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