36 theory BaseDefinitions imports Know_Store |
36 theory BaseDefinitions imports Know_Store |
37 ML_file termC.sml |
37 ML_file termC.sml |
38 ML_file substitution.sml |
38 ML_file substitution.sml |
39 ML_file contextC.sml |
39 ML_file contextC.sml |
40 ML_file environment.sml |
40 ML_file environment.sml |
41 *) "BaseDefinitions/BaseDefinitions" |
41 ( ** ) "BaseDefinitions/BaseDefinitions"( **) |
42 |
42 |
43 (* theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
43 (* theory Calculate imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
44 ML_file evaluate.sml |
44 ML_file evaluate.sml |
45 |
45 |
46 theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
46 theory ListC imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
48 theory Program imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
48 theory Program imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
49 theory Prog_Tac imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
49 theory Prog_Tac imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
50 theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
50 theory Tactical imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
51 theory Auto_Prog imports Program Prog_Tac Tactical begin |
51 theory Auto_Prog imports Program Prog_Tac Tactical begin |
52 theory ProgLang imports Prog_Expr Auto_Prog |
52 theory ProgLang imports Prog_Expr Auto_Prog |
53 *) "ProgLang/ProgLang" |
53 ( ** ) "ProgLang/ProgLang"( **) |
54 (* |
54 (* |
55 theory MathEngBasic imports |
55 theory MathEngBasic imports |
56 "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript" |
56 "~~/src/Tools/isac/ProgLang/ProgLang" "~~/src/Tools/isac/Specify/Input_Descript" |
57 ML_file thmC.sml |
57 ML_file thmC.sml |
58 ML_file problem.sml |
58 ML_file problem.sml |
75 ML_file "ctree-navi.sml" |
75 ML_file "ctree-navi.sml" |
76 ML_file ctree.sml |
76 ML_file ctree.sml |
77 |
77 |
78 ML_file "state-steps.sml" |
78 ML_file "state-steps.sml" |
79 ML_file calculation.sml |
79 ML_file calculation.sml |
80 *) "MathEngBasic/MathEngBasic" |
80 ( ** ) "MathEngBasic/MathEngBasic"( **) |
81 (* |
81 (* |
82 theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
82 theory Input_Descript imports "~~/src/Tools/isac/BaseDefinitions/BaseDefinitions" |
83 theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript |
83 theory Specify imports "~~/src/Tools/isac/ProgLang/ProgLang" Input_Descript |
84 ML_file formalise.sml |
84 ML_file formalise.sml |
85 ML_file "o-model.sml" |
85 ML_file "o-model.sml" |
94 ML_file "specify-step.sml" |
94 ML_file "specify-step.sml" |
95 ML_file calchead.sml (*..TODO review*) |
95 ML_file calchead.sml (*..TODO review*) |
96 ML_file "input-calchead.sml" |
96 ML_file "input-calchead.sml" |
97 ML_file "step-specify.sml" |
97 ML_file "step-specify.sml" |
98 ML_file specify.sml |
98 ML_file specify.sml |
99 *) "Specify/Specify" |
99 ( ** ) "Specify/Specify"( **) |
100 (* |
100 (* |
101 theory Interpret imports "~~/src/Tools/isac/Specify/Specify" |
101 theory Interpret imports "~~/src/Tools/isac/Specify/Specify" |
102 ML_file istate.sml |
102 ML_file istate.sml |
103 ML_file "sub-problem.sml" |
103 ML_file "sub-problem.sml" |
104 ML_file "thy-read.sml" |
104 ML_file "thy-read.sml" |
106 ML_file "error-pattern.sml" |
106 ML_file "error-pattern.sml" |
107 ML_file derive.sml |
107 ML_file derive.sml |
108 ML_file "li-tool.sml" |
108 ML_file "li-tool.sml" |
109 ML_file "lucas-interpreter.sml" |
109 ML_file "lucas-interpreter.sml" |
110 ML_file "step-solve.sml" |
110 ML_file "step-solve.sml" |
111 *) "Interpret/Interpret" |
111 ( ** ) "Interpret/Interpret"( **) |
112 (* |
112 (* |
113 theory MathEngine imports "~~/src/Tools/isac/Interpret/Interpret" |
113 theory MathEngine imports Interpret.Interpret |
114 ML_file "fetch-tactics.sml" |
114 ML_file "fetch-tactics.sml" |
115 ML_file solve.sml |
115 ML_file solve.sml |
116 ML_file step.sml |
116 ML_file step.sml |
117 ML_file "detail-step.sml" |
117 ML_file "detail-step.sml" |
118 ML_file "mathengine-stateless.sml" |
118 ML_file "mathengine-stateless.sml" |
119 ML_file messages.sml |
119 ML_file messages.sml |
120 ML_file states.sml |
120 ML_file states.sml |
121 *) "MathEngine/MathEngine" |
121 ( ** ) "MathEngine/MathEngine"( **) |
122 (* |
122 (* |
123 theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine" |
123 theory Test_Code imports "~~/src/Tools/isac/MathEngine/MathEngine" |
124 ML_file "test-code.sml" |
124 ML_file "test-code.sml" |
125 *) "Test_Code/Test_Code" |
125 ( ** ) "Test_Code/Test_Code"( **) |
126 (* |
126 (* |
127 theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine" |
127 theory BridgeLibisabelle imports "~~/src/Tools/isac/MathEngine/MathEngine" |
128 ML_file "thy-present.sml" |
128 ML_file "thy-present.sml" |
129 ML_file mathml.sml |
129 ML_file mathml.sml |
130 ML_file datatypes.sml |
130 ML_file datatypes.sml |
131 ML_file "pbl-met-hierarchy.sml" |
131 ML_file "pbl-met-hierarchy.sml" |
132 ML_file "thy-hierarchy.sml" |
132 ML_file "thy-hierarchy.sml" |
133 ML_file "interface-xml.sml" |
133 ML_file "interface-xml.sml" |
134 ML_file interface.sml |
134 ML_file interface.sml |
135 *) "BridgeLibisabelle/BridgeLibisabelle" |
135 ( ** ) "BridgeLibisabelle/BridgeLibisabelle"( **) |
136 (* |
136 (* |
137 theory Isac imports "~~/src/Tools/isac/MathEngine/MathEngine" |
137 theory Isac imports "~~/src/Tools/isac/MathEngine/MathEngine" |
138 ML_file parseC.sml |
138 ML_file parseC.sml |
139 theory BridgeJEdit imports Isac |
139 theory BridgeJEdit imports Isac |
140 *) "BridgeJEdit/BridgeJEdit" |
140 ( ** ) "BridgeJEdit/BridgeJEdit"( **) |
141 |
141 |
142 "Knowledge/Build_Thydata" (*imports Isac.thy etc*) |
142 "Knowledge/Build_Thydata" (*imports Isac.thy etc*) |
143 |
143 |
144 (*//-----------------------------------------------------------------------------------------\\*) |
144 (*//-----------------------------------------------------------------------------------------\\*) |
145 (*\\-----------------------------------------------------------------------------------------//*) |
145 (*\\-----------------------------------------------------------------------------------------//*) |
165 text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close> |
165 text \<open>contextthyOK2xml; (*"xmlsrc/interface-xml.sml"*)\<close> |
166 ML \<open>prog_expr\<close> |
166 ML \<open>prog_expr\<close> |
167 |
167 |
168 ML \<open>Prog_Expr.eval_occurs_in\<close> |
168 ML \<open>Prog_Expr.eval_occurs_in\<close> |
169 ML \<open>@{thm last_thmI}\<close> |
169 ML \<open>@{thm last_thmI}\<close> |
170 ML \<open>@{thm Querkraft_Belastung}\<close> |
170 (** )ML \<open>@{thm Querkraft_Belastung}\<close>( *exception FAIL NONE raised (line 161 of "General/scan.ML")*) |
171 |
171 |
172 ML \<open>Check_Unique.on := false;\<close> |
172 ML \<open>Check_Unique.on := false;\<close> |
173 ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close> |
173 ML \<open>writeln "**** isac kernel = math-engine + Knowledge complete ******"\<close> |
174 ML \<open>@{theory "Isac_Knowledge"}\<close> |
174 ML \<open>@{theory "Isac_Knowledge"}\<close> |
175 ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] |
175 ML \<open>(*get_the ["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"] |