| author | wneuper <Walther.Neuper@jku.at> |
| Wed, 11 Jan 2023 11:38:01 +0100 | |
| changeset 60650 | 06ec8abfd3bc |
| parent 60649 | b2ff1902420f |
| child 60705 | b719a0b7c6b5 |
| permissions | -rw-r--r-- |
1 (* Title: collect all defitions for the Lucas-Interpreter
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
4 *)
6 theory Specify
7 imports "$ISABELLE_ISAC/MathEngBasic/MathEngBasic"
8 keywords "cas" :: thy_decl
9 begin
10 ML_file "o-model.sml"
11 ML_file "i-model.sml"
12 ML_file "pre-conditions.sml"
13 ML_file "p-model.sml"
14 ML_file "m-match.sml"
15 ML_file refine.sml
16 ML_file "test-out.sml"
17 ML_file "specify-step.sml"
18 ML_file specification.sml
19 ML_file "cas-command.sml"
20 ML_file "p-spec.sml"
21 ML_file specify.sml
22 ML_file "sub-problem.sml"
23 ML_file "step-specify.sml"
25 ML \<open>
26 \<close> ML \<open>
27 \<close> ML \<open>
28 \<close> ML \<open>
29 \<close>
30 end