| author | wneuper <Walther.Neuper@jku.at> |
| Mon, 11 Dec 2023 17:26:30 +0100 | |
| changeset 60782 | e797d1bdfe37 |
| parent 60776 | c2e6848d3dce |
| permissions | -rw-r--r-- |
1 (* Title: "Specify/Specify.thy"
2 Author: Walther Neuper 110226
3 (c) due to copyright terms
5 Specification phase
6 *)
8 theory Specify
9 imports "$ISABELLE_ISAC/MathEngBasic/MathEngBasic"
10 keywords "cas" :: thy_decl
11 begin
12 ML_file "o-model.sml"
13 ML_file "pre-conditions.sml" (*uses Model_Def.i_model*)
14 ML_file "i-model.sml"
15 ML_file "p-model.sml"
16 ML_file "m-match.sml"
17 ML_file refine.sml
18 ML_file "test-out.sml"
19 ML_file "specify-step.sml"
20 ML_file specification.sml
21 ML_file "cas-command.sml"
22 ML_file "p-spec.sml"
23 ML_file specify.sml
24 ML_file "sub-problem.sml"
25 ML_file "step-specify.sml"
27 ML \<open>
28 \<close> ML \<open>
29 \<close> ML \<open>
30 \<close> ML \<open>
31 \<close> ML \<open>
32 \<close> ML \<open>
33 \<close> ML \<open>
34 \<close> ML \<open>
35 \<close> ML \<open>
36 I_Model.is_error: I_Model.feedback -> bool
37 \<close> ML \<open>
38 P_Model.mk_delete: theory -> string -> I_Model.feedback -> Tactic.input
39 \<close> ML \<open>
40 P_Model.mk_additem: string -> TermC.as_string -> Tactic.input
41 \<close> ML \<open>
42 \<close>
43 end