| author | wneuper <Walther.Neuper@jku.at> |
| Mon, 01 Jan 2024 11:31:16 +0100 | |
| changeset 60789 | 8fa678b678e8 |
| parent 60733 | 4097c1317986 |
| 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 Specify.Specify
10 begin
11 ML_file istate.sml
12 ML_file "li-tool.sml"
13 ML_file "solve-step.sml"
14 ML_file "error-pattern.sml"
15 ML_file derive.sml
16 ML_file "lucas-interpreter.sml"
17 ML_file "step-solve.sml"
19 ML \<open>
20 \<close> ML \<open>
22 \<close> ML \<open>
23 \<close>
24 end