test/Tools/isac/Test_Isac.thy
changeset 59919 3a7fb975af9d
parent 59917 e98d714cca1a
child 59920 33913fe24685
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Tue Apr 28 19:39:06 2020 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Apr 29 09:03:01 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 @@ -126,10 +125,9 @@
    1.12    open Rewrite;
    1.13    open Eval;                   get_pair;
    1.14    open TermC;                  atomt;
    1.15 -  open Celem;
    1.16    open Rule;
    1.17    open Rule_Set;               Sequence;
    1.18 -  open Exec_Def
    1.19 +  open Eval_Def
    1.20    open ThyC
    1.21    open ThmC_Def
    1.22    open ThmC
    1.23 @@ -180,7 +178,7 @@
    1.24    ML \<open>"%%%%%%%%%%%%%%%%% start ProgLang.thy %%%%%%%%%%%%%%%%%%%";\<close>
    1.25    ML_file "BaseDefinitions/libraryC.sml"
    1.26    ML_file "BaseDefinitions/rule-def.sml"
    1.27 -  ML_file "BaseDefinitions/exec-def.sml"
    1.28 +  ML_file "BaseDefinitions/eval-def.sml"
    1.29    ML_file "BaseDefinitions/rewrite-order.sml"
    1.30    ML_file "BaseDefinitions/theoryC.sml"
    1.31    ML_file "BaseDefinitions/rule.sml"
    1.32 @@ -250,7 +248,6 @@
    1.33  
    1.34    ML_file "Interpret/istate.sml"
    1.35    ML_file "Interpret/sub-problem.sml"
    1.36 -  ML_file "Interpret/rewtools.sml"
    1.37    ML_file "Interpret/error-pattern.sml"
    1.38    ML_file "Interpret/li-tool.sml"
    1.39    ML_file "Interpret/lucas-interpreter.sml"
    1.40 @@ -263,6 +260,7 @@
    1.41    ML_file "MathEngine/messages.sml"
    1.42    ML_file "MathEngine/states.sml"
    1.43  
    1.44 +  ML_file "BridgeLibisabelle/thy-present.sml"
    1.45    ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
    1.46    ML_file "BridgeLibisabelle/datatypes.sml"        (*TODO/part.*)
    1.47    ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"(*TODO after 2009-2/part.*)