test/Tools/isac/Test_Isac.thy
changeset 59359 107330cc8b6a
parent 59358 8509ca4e79ec
child 59361 76b3141b73ab
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Thu Feb 08 12:49:52 2018 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Feb 08 13:20:40 2018 +0100
     1.3 @@ -65,7 +65,9 @@
     1.4    "~~/test/Pure/Isar/Test_Parse_Term"
     1.5    "~~/test/HOL/Library/Test_Polynomial"
     1.6    "~~/test/Tools/isac/Interpret/ptyps"       (* setup for ptyps.sml    *)
     1.7 +  ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
     1.8    "~~/test/Tools/isac/ProgLang/calculate"    (* setup for calculate.sml*)
     1.9 +(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
    1.10    "~~/test/Tools/isac/ProgLang/scrtools"     (* setup for scrtools.sml *)
    1.11    "~~/test/Tools/isac/Knowledge/integrate"   (* setup for integrate.sml*)
    1.12  
    1.13 @@ -122,16 +124,9 @@
    1.14    ML_file          "kestore.sml"        (* setup in ADDTEST/accumulate-val/lucas_interpreter.sml*)
    1.15    ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
    1.16    ML_file "ProgLang/termC.sml"
    1.17 +  ML_file "ProgLang/calculate.sml"      (* requires setup from calculate.thy                    *)
    1.18  (*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
    1.19 -  ML_file "ProgLang/calculate.sml"      (* requires setup from calculate.thy *)
    1.20 -  ---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------*)
    1.21 -
    1.22 -ML {*
    1.23 -*} ML {*
    1.24 -*} ML {*
    1.25 -*}
    1.26    ML_file "ProgLang/rewrite.sml"
    1.27 -(*---------------------- do Minisubpbl before ADDTESTS/All_Ctxt --------------------------------
    1.28    ML_file "ProgLang/listC.sml"
    1.29    ML_file "ProgLang/scrtools.sml"
    1.30    ML_file "ProgLang/tools.sml"