14 theory Build_Isac |
14 theory Build_Isac |
15 imports |
15 imports |
16 (* theory Know_Store imports Complex_Main |
16 (* theory Know_Store imports Complex_Main |
17 ML_file libraryC.sml |
17 ML_file libraryC.sml |
18 ML_file theoryC.sml |
18 ML_file theoryC.sml |
19 ML_file unparseC.sml |
19 ML_file unparseC.sml |
20 ML_file "rule-def.sml" |
20 ML_file "rule-def.sml" |
21 ML_file thmC.sml |
21 ML_file "thmC-def.sml" |
22 ML_file "eval-def.sml" |
22 ML_file "eval-def.sml" |
23 ML_file "rewrite-order.sml" |
23 ML_file "rewrite-order.sml" |
24 ML_file rule.sml |
24 ML_file rule.sml |
25 ML_file "error-fill-def.sml" |
25 ML_file "error-pattern-def.sml" |
26 ML_file "rule-set.sml" |
26 ML_file "rule-set.sml" |
|
27 |
|
28 ML_file "store.sml" |
|
29 ML_file "check-unique.sml" |
|
30 ML_file "specification.sml" |
|
31 ML_file "model-pattern.sml" |
|
32 ML_file "problem-def.sml" |
|
33 ML_file "method-def.sml" |
|
34 ML_file "cas-def.sml" |
|
35 ML_file "thy-write.sml" |
27 theory BaseDefinitions imports Know_Store |
36 theory BaseDefinitions imports Know_Store |
28 ML_file termC.sml |
37 ML_file termC.sml |
|
38 ML_file substitution.sml |
29 ML_file contextC.sml |
39 ML_file contextC.sml |
30 ML_file environment.sml |
40 ML_file environment.sml |
31 *) "BaseDefinitions/BaseDefinitions" |
41 *) "BaseDefinitions/BaseDefinitions" |
32 |
42 |
33 (* theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
43 (* theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
43 *) "ProgLang/ProgLang" |
53 *) "ProgLang/ProgLang" |
44 (* |
54 (* |
45 theory MathEngBasic imports |
55 theory MathEngBasic imports |
46 "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript" |
56 "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript" |
47 ML_file thmC.sml |
57 ML_file thmC.sml |
|
58 ML_file problem.sml |
|
59 ML_file method.sml |
|
60 ML_file "cas-command.sml" |
|
61 |
48 ML_file rewrite.sml |
62 ML_file rewrite.sml |
|
63 |
|
64 ML_file "model-def.sml" |
|
65 ML_file "istate-def.sml" |
49 ML_file "calc-tree-elem.sml" |
66 ML_file "calc-tree-elem.sml" |
50 ML_file model.sml |
67 ML_file "pre-conds-def.sml" |
51 ML_file mstools.sml |
68 |
52 ML_file "specification-elems.sml" |
|
53 ML_file "istate-def.sml" |
|
54 ML_file tactic.sml |
69 ML_file tactic.sml |
|
70 ML_file applicable.sml |
|
71 |
55 ML_file position.sml |
72 ML_file position.sml |
56 ML_file "ctree-basic.sml" |
73 ML_file "ctree-basic.sml" |
57 ML_file "ctree-access.sml" |
74 ML_file "ctree-access.sml" |
58 ML_file "ctree-navi.sml" |
75 ML_file "ctree-navi.sml" |
59 ML_file ctree.sml |
76 ML_file ctree.sml |
60 (*ML_file tactic.sml*) |
77 |
|
78 ML_file "state-steps.sml" |
61 ML_file calculation.sml |
79 ML_file calculation.sml |
62 *) "MathEngBasic/MathEngBasic" |
80 *) "MathEngBasic/MathEngBasic" |
63 (* |
81 (* |
64 theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
82 theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
65 theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript |
83 theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript |
66 ML_file ptyps.sml |
84 ML_file formalise.sml |
67 ML_file generate.sml |
85 ML_file "o-model.sml" |
68 ML_file calchead.sml |
86 ML_file "i-model.sml" |
|
87 ML_file "p-model.sml" |
|
88 ML_file model.sml |
|
89 ML_file "pre-conditions.sml" |
|
90 ML_file refine.sml |
|
91 ML_file "mstools.sml" (*..TODO review*) |
|
92 ML_file ptyps.sml (*..TODO review*) |
|
93 ML_file "test-out.sml" |
|
94 ML_file "specify-step.sml" |
|
95 ML_file calchead.sml (*..TODO review*) |
|
96 ML_file "input-calchead.sml" |
69 ML_file "step-specify.sml" |
97 ML_file "step-specify.sml" |
70 ML_file specify.sml |
98 ML_file specify.sml |
71 *) "Specify/Specify" |
99 *) "Specify/Specify" |
72 (* |
100 (* |
73 theory Interpret imports "~~/src/Tools/isac/Specify/Specify" |
101 theory Interpret imports "~~/src/Tools/isac/Specify/Specify" |
74 ML_file istate.sml |
102 ML_file istate.sml |
75 ML_file rewtools.sml |
103 ML_file "sub-problem.sml" |
|
104 ML_file "thy-read.sml" |
|
105 ML_file "solve-step.sml" |
|
106 ML_file "error-pattern.sml" |
|
107 ML_file derive.sml |
76 ML_file "li-tool.sml" |
108 ML_file "li-tool.sml" |
77 ML_file inform.sml |
|
78 ML_file "lucas-interpreter.sml" |
109 ML_file "lucas-interpreter.sml" |
79 ML_file "step-solve.sml" |
110 ML_file "step-solve.sml" |
80 *) "Interpret/Interpret" |
111 *) "Interpret/Interpret" |
81 (* |
112 (* |
82 theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret" |
113 theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret" |
92 theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine" |
123 theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine" |
93 ML_file "test-code.sml" |
124 ML_file "test-code.sml" |
94 *) "Test_Code/Test_Code" |
125 *) "Test_Code/Test_Code" |
95 (* |
126 (* |
96 theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine" |
127 theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine" |
97 ML_file mathml.sml |
128 ML_file "thy-present.sml" |
|
129 ML_file mathml.sml |
98 ML_file datatypes.sml |
130 ML_file datatypes.sml |
99 ML_file "pbl-met-hierarchy.sml" |
131 ML_file "pbl-met-hierarchy.sml" |
100 ML_file "thy-hierarchy.sml" |
132 ML_file "thy-hierarchy.sml" |
101 ML_file "interface-xml.sml" |
133 ML_file "interface-xml.sml" |
102 ML_file interface.sml |
134 ML_file interface.sml |