test/Tools/isac/Test_Isac_Short.thy
changeset 59917 e98d714cca1a
parent 59914 ab5bd5c37e13
child 59919 3a7fb975af9d
     1.1 --- a/test/Tools/isac/Test_Isac_Short.thy	Tue Apr 28 16:51:36 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac_Short.thy	Tue Apr 28 17:50:18 2020 +0200
     1.3 @@ -100,7 +100,6 @@
     1.4    open Error_Pattern;
     1.5    open Error_Pattern_Def;
     1.6    open In_Chead;
     1.7 -  open Rtools;
     1.8    open Chead;                  pt_extract;
     1.9    open Generate;               (* NONE *)
    1.10    open Ctree;                  append_problem;
    1.11 @@ -250,7 +249,6 @@
    1.12  
    1.13    ML_file "Interpret/istate.sml"
    1.14    ML_file "Interpret/sub-problem.sml"
    1.15 -  ML_file "Interpret/rewtools.sml"
    1.16    ML_file "Interpret/error-pattern.sml"
    1.17    ML_file "Interpret/li-tool.sml"
    1.18    ML_file "Interpret/lucas-interpreter.sml"
    1.19 @@ -263,6 +261,7 @@
    1.20    ML_file "MathEngine/messages.sml"
    1.21    ML_file "MathEngine/states.sml"
    1.22  
    1.23 +  ML_file "BridgeLibisabelle/thy-present.sml"
    1.24    ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
    1.25    ML_file "BridgeLibisabelle/datatypes.sml"        (*TODO/part.*)
    1.26    ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)