1.1 --- a/test/Tools/isac/Test_Isac.thy	Fri Aug 05 11:41:06 2022 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Fri Aug 05 12:30:16 2022 +0200
     1.3 @@ -78,8 +78,8 @@
     1.4    "$ISABELLE_ISAC_TEST/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)
     1.5  (**) 
     1.6  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
     1.7 -  "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)
     1.8 -  "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)
     1.9 +  "$ISABELLE_ISAC/Knowledge/GCD_Poly_OLD" (*not imported by Isac.thy*)        (*Test_Isac_Short*)
    1.10 +  "$ISABELLE_ISAC/Knowledge/GCD_Poly_FP"  (*not imported by Isac.thy*)        (*Test_Isac_Short*)
    1.11  (*\---------------------- do Minisubpbl before ADDTESTS/All_Ctxt ------------------------------/*)
    1.12  (**)
    1.13  
    1.14 @@ -189,6 +189,7 @@
    1.15  (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
    1.16    ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
    1.17  
    1.18 +  ML_file "ProgLang/calculate.sml"
    1.19    ML_file "ProgLang/evaluate.sml"       (* requires setup from calculate.thy                    *)
    1.20    ML_file "ProgLang/listC.sml"
    1.21    ML_file "ProgLang/prog_expr.sml"
    1.22 @@ -261,12 +262,10 @@
    1.23  
    1.24    ML_file "BridgeLibisabelle/thy-present.sml"
    1.25    ML_file "BridgeLibisabelle/mathml.sml"           (*part.*)
    1.26 +  ML_file "BridgeLibisabelle/pbl-met-hierarchy.sml"
    1.27    ML_file "BridgeLibisabelle/thy-hierarchy.sml"
    1.28    ML_file "BridgeLibisabelle/interface-xml.sml"     (*TODO after 2009-2*)
    1.29    ML_file "BridgeLibisabelle/interface.sml"
    1.30 -(*WITHOUT inhibit exn WN1130621 Isabelle2012-->13 !thehier! THIS ERROR OCCURS:
    1.31 -  ... SAME ERROR HERE ON ISABELLE2012 AS IN ISAC ON ISABELLE2011*)
    1.32 -
    1.33    ML_file "BridgeJEdit/parseC.sml"
    1.34    ML_file "BridgeJEdit/preliminary.sml"
    1.35    ML_file "BridgeJEdit/vscode-example.sml"
    1.36 @@ -274,6 +273,8 @@
    1.37    ML_file "Knowledge/delete.sml"
    1.38    ML_file "Knowledge/descript.sml"
    1.39    ML_file "Knowledge/simplify.sml"
    1.40 +  ML_file "Knowledge/poly-1.sml"
    1.41 +ML_file "Knowledge/poly-2.sml"                                                (*Test_Isac_Short*)
    1.42    ML_file "Knowledge/gcd_poly_ml.sml"
    1.43    ML_file "Knowledge/rational-1.sml"
    1.44    ML_file "Knowledge/rational-2.sml"                                          (*Test_Isac_Short*)