test/Tools/isac/Test_Isac.thy
changeset 60624 0e0ac7706f0d
parent 60609 5967b6e610b5
child 60629 20c3d272d79c
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Dec 09 16:29:04 2022 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Dec 15 13:03:51 2022 +0100
     1.3 @@ -82,6 +82,7 @@
     1.4    "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        (*Test_Isac_Short*)
     1.5  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
     1.6  (**)
     1.7 +  "$ISABELLE_ISAC_TEST/Tools/isac/BridgeJEdit/Test_VSCode_Example"
     1.8  
     1.9  begin
    1.10  
    1.11 @@ -209,6 +210,7 @@
    1.12    ML_file "BaseDefinitions/theoryC.sml"
    1.13    ML_file "BaseDefinitions/rule.sml"
    1.14    ML_file "BaseDefinitions/thmC-def.sml"
    1.15 +  ML_file "BaseDefinitions/model-pattern.sml"
    1.16    ML_file "BaseDefinitions/error-fill-def.sml"
    1.17    ML_file "BaseDefinitions/rule-set.sml"
    1.18    ML_file "BaseDefinitions/check-unique.sml"
    1.19 @@ -259,9 +261,10 @@
    1.20  
    1.21  subsection \<open>further functionality alongside batch build sequence\<close>
    1.22    ML_file "MathEngBasic/thmC.sml"
    1.23 +  ML_file "MathEngBasic/problem.sml"
    1.24    ML_file "MathEngBasic/rewrite.sml"
    1.25    ML_file "MathEngBasic/tactic.sml"
    1.26 -  ML_file "MathEngBasic/ctree.sml"
    1.27 +  ML_file "MathEngBasic/ctree.sml" (*if red, get the file into a text buffer -- this might clear*)
    1.28    ML_file "MathEngBasic/calculation.sml"
    1.29  
    1.30    ML_file "Specify/formalise.sml"
    1.31 @@ -300,6 +303,7 @@
    1.32    ML_file "BridgeLibisabelle/thy-hierarchy.sml"
    1.33    ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009-2*)
    1.34    ML_file "BridgeLibisabelle/interface.sml"
    1.35 +
    1.36    ML_file "BridgeJEdit/parseC.sml"
    1.37    ML_file "BridgeJEdit/preliminary.sml"
    1.38    ML_file "BridgeJEdit/vscode-example.sml"