| author | Walther Neuper <walther.neuper@jku.at> |
| Tue, 10 Sep 2019 16:13:28 +0200 | |
| changeset 59613 | 8d28eab80f7f |
| parent 59612 | 14b7eae04d42 |
| child 59616 | eb9db079bca4 |
| permissions | -rw-r--r-- |
| neuper@41905 | 1 |
(* Title: collect all defitions for xml generation |
| neuper@41905 | 2 |
Author: Walther Neuper 110226 |
| neuper@41905 | 3 |
(c) due to copyright terms |
| neuper@41905 | 4 |
*) |
| neuper@41905 | 5 |
|
| wneuper@59600 | 6 |
theory BridgeLibisabelle |
| walther@59612 | 7 |
imports "~~/src/Tools/isac/MathEngine/MathEngine" |
| neuper@52139 | 8 |
|
| neuper@41905 | 9 |
begin |
| wneuper@59600 | 10 |
ML_file mathml.sml |
| wneuper@59600 | 11 |
ML_file datatypes.sml |
| wneuper@59600 | 12 |
ML_file "pbl-met-hierarchy.sml" |
| wneuper@59600 | 13 |
ML_file "thy-hierarchy.sml" |
| walther@59613 | 14 |
ML_file "interface-xml.sml" |
| walther@59613 | 15 |
ML_file interface.sml |
| wneuper@59276 | 16 |
(*declare [[ML_print_depth = 999]]*) |
| wneuper@59458 | 17 |
ML \<open> |
| wneuper@59458 | 18 |
\<close> ML \<open> |
| walther@59613 | 19 |
"XML.tree" |
| walther@59613 | 20 |
(*//---------------------------------- rm libisabelle ---------------------------------------\\* ) |
| walther@59613 | 21 |
( *\\---------------------------------- rm libisabelle ---------------------------------------//*) |
| walther@59613 | 22 |
\<close> ML \<open> |
| wneuper@59458 | 23 |
\<close> |
| wneuper@59155 | 24 |
|
| wneuper@59216 | 25 |
end |