102 open Ctree; append_problem; |
102 open Ctree; append_problem; |
103 open Prog_Tac; |
103 open Prog_Tac; |
104 open Tactical; |
104 open Tactical; |
105 open Prog_Expr; |
105 open Prog_Expr; |
106 (*open Auto_Prog;*) |
106 (*open Auto_Prog;*) |
|
107 open Input_Descript; |
107 open Specify; show_ptyps; |
108 open Specify; show_ptyps; |
108 open Applicable; mk_set; |
109 open Applicable; mk_set; |
109 open Solve; (* NONE *) |
110 open Solve; (* NONE *) |
110 open Selem; e_fmz; |
111 open Selem; e_fmz; |
111 open Stool; (* NONE *) |
112 open Stool; (* NONE *) |
215 ML_file "Knowledge/rational.sml" |
216 ML_file "Knowledge/rational.sml" |
216 ML_file "Knowledge/equation.sml" |
217 ML_file "Knowledge/equation.sml" |
217 ML_file "Knowledge/root.sml" |
218 ML_file "Knowledge/root.sml" |
218 ML_file "Knowledge/lineq.sml" |
219 ML_file "Knowledge/lineq.sml" |
219 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
220 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *) |
220 ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *) |
221 ML_file "Knowledge/rateq.sml" (*exception Size raised "./basis/LibrarySupport.sml")*) |
221 ML_file "Knowledge/rootrat.sml" |
222 ML_file "Knowledge/rootrat.sml" |
222 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
223 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *) |
223 ML_file "Knowledge/partial_fractions.sml" |
224 ML_file "Knowledge/partial_fractions.sml" |
224 ML_file "Knowledge/polyeq.sml" |
225 (*ML_file "Knowledge/polyeq.sml" exception Size raised "./basis/LibrarySupport.sml")*) |
225 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *) |
226 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *) |
226 ML_file "Knowledge/calculus.sml" |
227 ML_file "Knowledge/calculus.sml" |
227 ML_file "Knowledge/trig.sml" |
228 ML_file "Knowledge/trig.sml" |
228 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) |
229 (*ML_file "Knowledge/logexp.sml" not included as stuff for presentation of authoring*) |
229 ML_file "Knowledge/diff.sml" |
230 ML_file "Knowledge/diff.sml" |
231 ML_file "Knowledge/eqsystem.sml" |
232 ML_file "Knowledge/eqsystem.sml" |
232 ML_file "Knowledge/test.sml" |
233 ML_file "Knowledge/test.sml" |
233 ML_file "Knowledge/polyminus.sml" |
234 ML_file "Knowledge/polyminus.sml" |
234 ML_file "Knowledge/vect.sml" |
235 ML_file "Knowledge/vect.sml" |
235 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *) |
236 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *) |
236 ML_file "Knowledge/biegelinie-1.sml" |
237 ML_file "Knowledge/biegelinie-1.sml" (* exception Size raised "./basis/LibrarySupport.sml"*) |
237 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *) |
238 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *) |
238 ML_file "Knowledge/biegelinie-3.sml" |
239 ML_file "Knowledge/biegelinie-3.sml" (* exception Size raised "./basis/LibrarySupport.sml"*) |
239 ML_file "Knowledge/algein.sml" |
240 ML_file "Knowledge/algein.sml" |
240 ML_file "Knowledge/diophanteq.sml" |
241 ML_file "Knowledge/diophanteq.sml" |
241 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml" |
242 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml" |
242 ML_file "Knowledge/inssort.sml" |
243 ML_file "Knowledge/inssort.sml" |
243 ML_file "Knowledge/isac.sml" |
244 ML_file "Knowledge/isac.sml" |
244 ML_file "Knowledge/build_thydata.sml" |
245 ML_file "Knowledge/build_thydata.sml" |
245 |
246 |
246 section \<open>tests additional to src/.. files\<close> |
247 section \<open>further tests additional to src/.. files\<close> |
247 ML_file "BridgeLibisabelle/use-cases.sml" |
248 ML_file "BridgeLibisabelle/use-cases.sml" |
248 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml" |
249 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml" |
249 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml" |
250 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml" |
250 |
251 |
251 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |
252 ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close> |