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