theory Thy_All

 imports Thy_3 Thy_5 

 begin

 text {* how can we accumulate values, e.g. the methods alongside thy development dependencies ?

         ---------------------------------------------------------------------------------------

 *}

 ML {*

 *} ML {*

 KEStore_Elems.get_rlss @{theory}

 (*|> map check_kestore_rls 

   |> enumerate_strings

   |> map writeln*)

 (*

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

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

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

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

 *)

 *} ML {*

 case KEStore_Elems.get_rlss @{theory} of

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

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

 ;

 *} ML {*

 case KEStore_Elems.get_calcs @{theory} of

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

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

 *}

 end