equal
deleted
inserted
replaced
1 (* Title: tests for KEStore.thy |
1 (* Title: tests for Know_Store.thy |
2 Author: Walther Neuper |
2 Author: Walther Neuper |
3 Use is subject to license terms. |
3 Use is subject to license terms. |
4 *) |
4 *) |
5 |
5 |
6 "-----------------------------------------------------------------------------"; |
6 "-----------------------------------------------------------------------------"; |
13 "-----------------------------------------------------------------------------"; |
13 "-----------------------------------------------------------------------------"; |
14 |
14 |
15 "-------- fun check_kestore_rls ----------------------------------------------"; |
15 "-------- fun check_kestore_rls ----------------------------------------------"; |
16 "-------- fun check_kestore_rls ----------------------------------------------"; |
16 "-------- fun check_kestore_rls ----------------------------------------------"; |
17 "-------- fun check_kestore_rls ----------------------------------------------"; |
17 "-------- fun check_kestore_rls ----------------------------------------------"; |
18 if check_kestore_rls ("empty", ("KEStore", Rule_Set.empty)) = |
18 if check_kestore_rls ("empty", ("Know_Store", Rule_Set.empty)) = |
19 "(empty, (KEStore, Rls {#calc = 0, #rules = 0, ...))" |
19 "(empty, (Know_Store, Rls {#calc = 0, #rules = 0, ...))" |
20 then () else error "check_kestore_rls changed" |
20 then () else error "check_kestore_rls changed" |
21 ; |
21 ; |
22 Test_KEStore_Elems.get_rlss @{theory Isac_Knowledge} |
22 Test_KEStore_Elems.get_rlss @{theory Isac_Knowledge} |
23 |> map check_kestore_rls |
23 |> map check_kestore_rls |
24 |> enumerate_strings |
24 |> enumerate_strings |