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.*)