| author | Walther Neuper <walther.neuper@jku.at> |
| Fri, 24 Apr 2020 08:51:05 +0200 | |
| changeset 59909 | 821f038df564 |
| parent 59906 | cc8df204dcb6 |
| child 59916 | 2c0c34b18050 |
| permissions | -rw-r--r-- |
1 (* Title: Interpret/Interpret.thy
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 Collect all defitions for the Lucas-Interpreter
6 *)
8 theory Interpret
9 imports "~~/src/Tools/isac/Specify/Specify"
10 begin
11 (* removed all warnings here, only "handle _" remains *)
12 ML_file istate.sml
13 ML_file "sub-problem.sml"
14 ML_file rewtools.sml
15 ML_file "error-pattern.sml"
16 ML_file derive.sml
17 ML_file "li-tool.sml"
18 ML_file "lucas-interpreter.sml"
19 ML_file "step-solve.sml"
20 ML \<open>
21 \<close> ML \<open>
22 \<close> ML \<open>
23 \<close>
24 end