test/Tools/isac/Test_Isac_Short.thy
changeset 60384 2b6e73df4e5d
parent 60354 716dd4a05cc8
child 60387 8e46f61fdb15
equal deleted inserted replaced
60383:fd186011fcd6 60384:2b6e73df4e5d
   187   ML_file "BaseDefinitions/check-unique.sml"
   187   ML_file "BaseDefinitions/check-unique.sml"
   188 (*called by Know_Store..*)
   188 (*called by Know_Store..*)
   189   ML_file "BaseDefinitions/calcelems.sml"
   189   ML_file "BaseDefinitions/calcelems.sml"
   190   ML_file "BaseDefinitions/termC.sml"
   190   ML_file "BaseDefinitions/termC.sml"
   191   ML_file "BaseDefinitions/substitution.sml"
   191   ML_file "BaseDefinitions/substitution.sml"
   192   ML_file "BaseDefinitions/contextC.sml"
   192 (*ML_file "BaseDefinitions/contextC.sml"  TOODOO.1 broken with real_unary_minus *)
   193   ML_file "BaseDefinitions/environment.sml"
   193   ML_file "BaseDefinitions/environment.sml"
   194 (** )ML_file "BaseDefinitions/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 
   197 
   229   ML_file "Minisubpbl/790-complete.sml"
   229   ML_file "Minisubpbl/790-complete.sml"
   230   ML_file "Minisubpbl/800-append-on-Frm.sml"
   230   ML_file "Minisubpbl/800-append-on-Frm.sml"
   231 
   231 
   232 subsection \<open>further functionality alongside batch build sequence\<close>
   232 subsection \<open>further functionality alongside batch build sequence\<close>
   233   ML_file "MathEngBasic/thmC.sml"
   233   ML_file "MathEngBasic/thmC.sml"
   234   ML_file "MathEngBasic/rewrite.sml"
   234 (*ML_file "MathEngBasic/rewrite.sml"   TOODOO.1 loops with real_unary_minus *)
   235   ML_file "MathEngBasic/tactic.sml"
   235   ML_file "MathEngBasic/tactic.sml"
   236   ML_file "MathEngBasic/ctree.sml"
   236 (*ML_file "MathEngBasic/ctree.sml"   TOODOO.1 loops with real_unary_minus *)
   237   ML_file "MathEngBasic/calculation.sml"
   237   ML_file "MathEngBasic/calculation.sml"
   238 
   238 
   239   ML_file "Specify/formalise.sml"
   239   ML_file "Specify/formalise.sml"
   240   ML_file "Specify/o-model.sml"
   240   ML_file "Specify/o-model.sml"
   241   ML_file "Specify/i-model.sml"
   241   ML_file "Specify/i-model.sml"
   251   ML_file "Specify/specify.sml"
   251   ML_file "Specify/specify.sml"
   252   ML_file "Specify/step-specify.sml"
   252   ML_file "Specify/step-specify.sml"
   253 
   253 
   254   ML_file "Interpret/istate.sml"
   254   ML_file "Interpret/istate.sml"
   255   ML_file "Interpret/sub-problem.sml"
   255   ML_file "Interpret/sub-problem.sml"
   256   ML_file "Interpret/error-pattern.sml"
   256 (*ML_file "Interpret/error-pattern.sml"   TOODOO.1 loops with real_unary_minus *)
   257   ML_file "Interpret/li-tool.sml"
   257   ML_file "Interpret/li-tool.sml"
   258   ML_file "Interpret/lucas-interpreter.sml"
   258   ML_file "Interpret/lucas-interpreter.sml"
   259   ML_file "Interpret/step-solve.sml"
   259   ML_file "Interpret/step-solve.sml"
   260 
   260 
   261   ML_file "MathEngine/me-misc.sml"
   261   ML_file "MathEngine/me-misc.sml"
   269   ML_file "BridgeLibisabelle/thy-present.sml"
   269   ML_file "BridgeLibisabelle/thy-present.sml"
   270   ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
   270   ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
   271   ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
   271   ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
   272   ML_file "BridgeLibisabelle/thy-hierarchy.sml"
   272   ML_file "BridgeLibisabelle/thy-hierarchy.sml"
   273   ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009- 2*)
   273   ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009- 2*)
   274   ML_file "BridgeLibisabelle/interface.sml"
   274 (*ML_file "BridgeLibisabelle/interface.sml"   TOODOO.1 loops with real_unary_minus *)
   275   ML_file "BridgeJEdit/parseC.sml"
   275   ML_file "BridgeJEdit/parseC.sml"
   276   ML_file "BridgeJEdit/preliminary.sml"
   276   ML_file "BridgeJEdit/preliminary.sml"
   277 
   277 
   278   ML_file "Knowledge/delete.sml"
   278   ML_file "Knowledge/delete.sml"
   279   ML_file "Knowledge/descript.sml"
   279   ML_file "Knowledge/descript.sml"
   282 (*ML_file "Knowledge/poly-2.sml"                                                Test_Isac_Short*)
   282 (*ML_file "Knowledge/poly-2.sml"                                                Test_Isac_Short*)
   283   ML_file "Knowledge/gcd_poly_ml.sml"
   283   ML_file "Knowledge/gcd_poly_ml.sml"
   284   ML_file "Knowledge/rational-1.sml"
   284   ML_file "Knowledge/rational-1.sml"
   285 (*ML_file "Knowledge/rational-2.sml"                                            Test_Isac_Short*)
   285 (*ML_file "Knowledge/rational-2.sml"                                            Test_Isac_Short*)
   286   ML_file "Knowledge/equation.sml"
   286   ML_file "Knowledge/equation.sml"
   287 (*ML_file "Knowledge/root.sml"                                                        see TOODOO.1*)
   287   ML_file "Knowledge/root.sml"
   288   ML_file "Knowledge/lineq.sml"
   288   ML_file "Knowledge/lineq.sml"
   289 
   289 
   290 (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
   290 (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
   291 (*ML_file "Knowledge/rateq.sml"     some complicated equations not recovered----Test_Isac_Short*)
   291 (*ML_file "Knowledge/rateq.sml"     some complicated equations not recovered----Test_Isac_Short*)
   292 (*ML_file "Knowledge/rootrat.sml"                           TOODOO.1 error inherited from root.sml*)
   292 (*ML_file "Knowledge/rootrat.sml"                           TOODOO.1 error inherited from root.sml*)
   318   ML_file "Knowledge/build_thydata.sml"
   318   ML_file "Knowledge/build_thydata.sml"
   319 
   319 
   320   ML_file "Test_Code/test-code.sml"
   320   ML_file "Test_Code/test-code.sml"
   321 
   321 
   322 section \<open>further tests additional to src/.. files\<close>
   322 section \<open>further tests additional to src/.. files\<close>
   323  ML_file "BridgeLibisabelle/use-cases.sml"
   323 (*ML_file "BridgeLibisabelle/use-cases.sml"   TOODOO.1 loops with real_unary_minus *)
   324 
   324 
   325   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   325   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   326   ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   326   ML \<open>"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   327   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   327   ML \<open>"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";\<close>
   328 ML \<open>
   328 ML \<open>