1 (* Title: collect all defitions for the Frontend |
1 (* Title: collect all defitions for the Frontend |
2 Author: Walther Neuper 110226 |
2 Author: Walther Neuper 110226 |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 |
5 |
6 theory Frontend imports |
6 theory Frontend imports "~~/src/Tools/isac/xmlsrc/xmlsrc" |
7 "~~/src/Tools/isac/xmlsrc/xmlsrc" |
|
8 uses |
|
9 ("~~/src/Tools/isac/Frontend/messages.sml") |
|
10 ("~~/src/Tools/isac/Frontend/states.sml") |
|
11 ("~~/src/Tools/isac/Frontend/interface.sml") |
|
12 ("~~/src/Tools/isac/print_exn_G.sml") |
|
13 begin |
7 begin |
|
8 ML {* val Rls {rules = rrr, ...} = assoc_rls "list_rls" *} |
|
9 ML {* length rrr = 53 *} |
|
10 ML {* AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *} |
|
11 ML {* val SOME (_, (Rls {rules = kkk, ...})) = |
|
12 AList.lookup op = (KEStore_Elems.get_rlss @{theory}) "list_rls" *} |
|
13 ML {* length kkk = 42 *} |
|
14 |
14 ML_file "~~/src/Tools/isac/Frontend/messages.sml" |
15 ML_file "~~/src/Tools/isac/Frontend/messages.sml" |
15 ML_file "~~/src/Tools/isac/Frontend/states.sml" |
16 ML_file "~~/src/Tools/isac/Frontend/states.sml" |
16 ML_file "~~/src/Tools/isac/Frontend/interface.sml" |
17 ML_file "~~/src/Tools/isac/Frontend/interface.sml" |
17 |
18 |
18 ML_file "~~/src/Tools/isac/print_exn_G.sml" |
19 use "~~/src/Tools/isac/print_exn_G.sml" |
19 end |
20 end |