test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy
changeset 55359 73dc85c025ab
parent 52156 aa0884017d48
child 59410 2cbb98890190
     1.1 --- a/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Mon Jan 27 13:40:36 2014 +0100
     1.2 +++ b/test/Tools/isac/ADDTESTS/accumulate-val/Thy_1.thy	Mon Jan 27 21:49:27 2014 +0100
     1.3 @@ -1,19 +1,19 @@
     1.4  theory Thy_1 imports Lucas_Interpreter begin
     1.5  
     1.6  ML {* 
     1.7 -  (* CHECK length (KEStore_Elems.get_rlss @{theory}) = length (! ruleset') 
     1.8 +  (* CHECK length (Test_KEStore_Elems.get_rlss @{theory}) = length (! ruleset') 
     1.9      AT THE BOTTOM OF A THEORY:*)
    1.10 -  length (KEStore_Elems.get_rlss @{theory}) = 0;
    1.11 +  length (Test_KEStore_Elems.get_rlss @{theory}) = 0;
    1.12  (*length (! test_ruleset')                  = 1 (* if you have clicked somewhere below *)*)
    1.13  *}
    1.14 -setup {* KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
    1.15 +setup {* Test_KEStore_Elems.add_rlss [("test_list_rls", (Context.theory_name @{theory}, Erls))] *}
    1.16  ML {* 
    1.17  (*test_ruleset' := overwritelthy @{theory} (! test_ruleset', [("test_list_rls", Erls)])
    1.18    ;
    1.19 -  if length (KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
    1.20 -    else error "removal of Unsynchonized.ref: ruleset' <> KEStore_Elems.get_rlss in Thy_1"*)
    1.21 +  if length (Test_KEStore_Elems.get_rlss @{theory}) = length (! test_ruleset') then ()
    1.22 +    else error "removal of Unsynchonized.ref: ruleset' <> Test_KEStore_Elems.get_rlss in Thy_1"*)
    1.23  *}
    1.24  
    1.25 -setup {* KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
    1.26 +setup {* Test_KEStore_Elems.add_calcs [("calc", ("Thy_1", e_evalfn))] *}
    1.27  
    1.28  end