1 theory Thy_All imports Thy_3 Thy_5 begin |
1 theory Thy_All imports Thy_3 Thy_5 begin |
2 |
2 |
3 ML {* |
3 ML {* |
4 KEStore_Elems.get_rlss @{theory} |
4 Test_KEStore_Elems.get_rlss @{theory} |
5 (*|> map check_kestore_rls |
5 (*|> map check_kestore_rls |
6 |> enumerate_strings |
6 |> enumerate_strings |
7 |> map writeln*) |
7 |> map writeln*) |
8 (* |
8 (* |
9 (rls2, (Thy_4, Erls))--1 |
9 (rls2, (Thy_4, Erls))--1 |
10 (rls1, (Thy_4, Erls))--2 |
10 (rls1, (Thy_4, Erls))--2 |
11 (rls, (Thy_5, Erls))--3 |
11 (rls, (Thy_5, Erls))--3 |
12 (test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4 |
12 (test_list_rls, (Thy_3, Rls {#calc = 0, #rules = 1, ...))--4 |
13 *) |
13 *) |
14 ; |
14 ; |
15 case KEStore_Elems.get_rlss @{theory} of |
15 case Test_KEStore_Elems.get_rlss @{theory} of |
16 ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Erls)) :: _ => () |
16 ("rls2", ("Thy_4", Erls)) :: ("rls1", ("Thy_4", Erls)) :: _ => () |
17 | _ => raise error "KEStore_Elems.get_rlss changed" |
17 | _ => raise error "Test_KEStore_Elems.get_rlss changed" |
18 ; |
18 ; |
19 case KEStore_Elems.get_calcs @{theory} of |
19 case Test_KEStore_Elems.get_calcs @{theory} of |
20 [("calc", ("Thy_1", _))] => () |
20 [("calc", ("Thy_1", _))] => () |
21 | _ => raise error "KEStore_Elems.get_calcs changed" |
21 | _ => raise error "Test_KEStore_Elems.get_calcs changed" |
22 *} |
22 *} |
23 |
23 |
24 end |
24 end |