| author | Walther Neuper <walther.neuper@jku.at> |
| Mon, 05 Oct 2020 12:16:16 +0200 | |
| changeset 60077 | bd5be37901f8 |
| parent 59983 | f1fdb213717b |
| child 60756 | b1ae5a019fa1 |
| permissions | -rw-r--r-- |
1 (* Title: MathEngine/MathEngine.thy
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
4 *)
6 theory MathEngine
7 imports Interpret.Interpret
8 begin
9 ML_file "me-misc.sml"
10 ML_file "fetch-tactics.sml"
11 ML_file solve.sml
12 ML_file step.sml
13 ML_file "detail-step.sml"
14 ML_file "mathengine-stateless.sml"
15 ML_file messages.sml
16 ML_file states.sml
18 ML \<open>
19 \<close> ML \<open>
20 \<close> ML \<open>
21 \<close>
22 end