theory Thy_1 imports Lucas_Interpreter begin

 ML {* 

   (* CHECK length (Test_KEStore_Elems.get_rlss @{theory}) = length (! ruleset') 

     AT THE BOTTOM OF A THEORY:*)

   length (Test_KEStore_Elems.get_rlss @{theory}) = 0;

 (*length (! test_ruleset')                  = 1 (* if you have clicked somewhere below *)*)

 *}

 setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}

 ML {* 

 (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])

   ;

   if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()

     else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)

 *}

 setup {* Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}

 end