theory Thy_All imports Thy_3 Thy_5 begin

 ML {*

 Test_KEStore_Elems.get_rlss @{theory}

 (*|> map check_kestore_rls 

   |> enumerate_strings

   |> map writeln*)

 (*

 (rls2, (Thy_4, Erls))--1 

 (rls1, (Thy_4, Erls))--2 

 (rls, (Thy_5, Erls))--3 

 (test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4 

 *)

 ;

 case Test_KEStore_Elems.get_rlss @{theory} of

   ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Erls)) :: _ => ()

 | _ => raise error "Test_KEStore_Elems.get_rlss changed"

 ;

 case Test_KEStore_Elems.get_calcs @{theory} of

   [("calc", ("Thy_1", _))] => ()

 | _ => raise error "Test_KEStore_Elems.get_calcs changed"

 *}

 end