| author | Walther Neuper <walther.neuper@jku.at> |
| Mon, 06 Apr 2020 11:44:36 +0200 | |
| changeset 59851 | 4dd533681fef |
| parent 59850 | f3cac3053e7b |
| child 59853 | e18f30c44998 |
| permissions | -rw-r--r-- |
| neuper@52146 | 1 |
theory Thy_1 imports Lucas_Interpreter begin |
| neuper@48809 | 2 |
|
| wneuper@59472 | 3 |
ML \<open> |
| s1210629013@55359 | 4 |
(* CHECK length (Test_KEStore_Elems.get_rlss @{theory}) = length (! ruleset')
|
| neuper@52126 | 5 |
AT THE BOTTOM OF A THEORY:*) |
| s1210629013@55359 | 6 |
length (Test_KEStore_Elems.get_rlss @{theory}) = 0;
|
| neuper@52156 | 7 |
(*length (! test_ruleset') = 1 (* if you have clicked somewhere below *)*) |
| wneuper@59472 | 8 |
\<close> |
| walther@59851 | 9 |
setup \<open>Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Rule_Set.Empty))]\<close>
|
| wneuper@59472 | 10 |
ML \<open> |
| walther@59851 | 11 |
(*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Rule_Set.Empty)])
|
| neuper@52126 | 12 |
; |
| s1210629013@55359 | 13 |
if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
|
| s1210629013@55359 | 14 |
else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*) |
| wneuper@59472 | 15 |
\<close> |
| neuper@52126 | 16 |
|
| walther@59850 | 17 |
setup \<open>Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", Rule_Set.e_evalfn))]\<close>
|
| neuper@48809 | 18 |
|
| neuper@48794 | 19 |
end |