4 |
4 |
5 theory Build_Thydata |
5 theory Build_Thydata |
6 imports Isac "~~/src/Tools/isac/ProgLang/ProgLang" |
6 imports Isac "~~/src/Tools/isac/ProgLang/ProgLang" |
7 Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*) |
7 Test_Build_Thydata (*for test/../build_thydata.sml, thy_hierarchy.sml*) |
8 begin |
8 begin |
9 |
|
10 ML {* |
|
11 (*writeln ("======= length (KEStore_Elems = " ^ |
|
12 (KEStore_Elems.get_mets @{theory} |> count_kestore_ptyps |> string_of_int)); |
|
13 writeln ("======= length (! mets) = " ^ |
|
14 (count_kestore_ptyps (! mets) |> string_of_int)); |
|
15 |
|
16 (* when creating session Isac see output in ~/.isabelle/../log/Isac *) |
|
17 writeln "======= begin KEStore_Elems.get_mets @{theory} ======="; |
|
18 KEStore_Elems.get_mets @{theory} |> map check_kestore_met; |
|
19 KEStore_Elems.get_mets @{theory} |
|
20 |> map check_kestore_met |> map writeln; |
|
21 writeln "\n\n======= KEStore_Elems.get_mets @{theory} ordered ======="; |
|
22 KEStore_Elems.get_mets @{theory} |> sort_kestore_met |> sort ptyp_ord |
|
23 |> map check_kestore_met |> enumerate_strings |> sort string_ord |> map writeln; |
|
24 writeln "======= end KEStore_Elems.get_mets @{theory} ======="; |
|
25 |
|
26 (* use a diff-tool for comparing KEStore_Elems.get_cas <--> ! xxx *) |
|
27 writeln "======= begin ! mets ======="; |
|
28 ! mets |> map check_kestore_met |> map writeln; |
|
29 writeln "\n\n======= ! mets ordered ======="; |
|
30 ! mets |> sort_kestore_met |> sort ptyp_ord |
|
31 |> map check_kestore_met |> enumerate_strings |> sort string_ord |> map writeln; |
|
32 writeln "======= end ! mets =======";*) |
|
33 *} |
|
34 |
9 |
35 subsection {* Build <Theory>-Data *} |
10 subsection {* Build <Theory>-Data *} |
36 text {* |
11 text {* |
37 <Theory>-Data represent Isac's "deductive knowledge" (whereas <Problems> and <Methods> |
12 <Theory>-Data represent Isac's "deductive knowledge" (whereas <Problems> and <Methods> |
38 represent application-oriented and algorithmic knowledge respectively.) <Theory>-Data |
13 represent application-oriented and algorithmic knowledge respectively.) <Theory>-Data |