176 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
176 ML \<open>"%%%%%%%%%%%%%%%%% end Isabelle %%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
177 |
177 |
178 section \<open>test ML Code of isac\<close> |
178 section \<open>test ML Code of isac\<close> |
179 subsection \<open>basic code first\<close> |
179 subsection \<open>basic code first\<close> |
180 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close> |
180 ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close> |
181 ML_file "CalcElements/libraryC.sml" |
181 ML_file "BaseDefinitions/libraryC.sml" |
182 ML_file "CalcElements/rule-def.sml" |
182 ML_file "BaseDefinitions/rule-def.sml" |
183 ML_file "CalcElements/exec-def.sml" |
183 ML_file "BaseDefinitions/exec-def.sml" |
184 ML_file "CalcElements/rewrite-order.sml" |
184 ML_file "BaseDefinitions/rewrite-order.sml" |
185 ML_file "CalcElements/theoryC.sml" |
185 ML_file "BaseDefinitions/theoryC.sml" |
186 ML_file "CalcElements/rule.sml" |
186 ML_file "BaseDefinitions/rule.sml" |
187 ML_file "CalcElements/thmC-def.sml" |
187 ML_file "BaseDefinitions/thmC-def.sml" |
188 ML_file "CalcElements/error-fill-def.sml" |
188 ML_file "BaseDefinitions/error-fill-def.sml" |
189 ML_file "CalcElements/rule-set.sml" |
189 ML_file "BaseDefinitions/rule-set.sml" |
190 ML_file "CalcElements/calcelems.sml" |
190 ML_file "BaseDefinitions/calcelems.sml" |
191 ML_file "CalcElements/termC.sml" |
191 ML_file "BaseDefinitions/termC.sml" |
192 ML_file "CalcElements/contextC.sml" |
192 ML_file "BaseDefinitions/contextC.sml" |
193 ML_file "CalcElements/environment.sml" |
193 ML_file "BaseDefinitions/environment.sml" |
194 ML_file "CalcElements/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) |
194 ML_file "BaseDefinitions/kestore.sml" (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*) |
195 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- |
195 (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt -------------------------------- |
196 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) |
196 ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*) |
197 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) |
197 ML_file "ProgLang/calculate.sml" (* requires setup from calculate.thy *) |
198 ML_file "ProgLang/listC.sml" |
198 ML_file "ProgLang/listC.sml" |
199 ML_file "ProgLang/prog_expr.sml" |
199 ML_file "ProgLang/prog_expr.sml" |