1.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Jul 24 16:06:06 2013 +0200
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Thu Jul 25 07:36:31 2013 +0200
     1.3 @@ -13,6 +13,9 @@
     1.4  $ ./bin/isabelle jedit -l Isac test/Tools/isac/Test_Isac.thy &
     1.5  *)
     1.6  
     1.7 +(*ATTENTION: "Knowledge/biegelinie.sml" NEEDS MANUAL INTERVENTION: 
     1.8 +  Tracing paused.  Stop, or continue with next 100, 1000, 10000 messages?*)
     1.9 +
    1.10  theory Test_Isac imports Isac
    1.11    "ADDTESTS/Ctxt"
    1.12    "ADDTESTS/test-depend/Build_Test"
    1.13 @@ -22,9 +25,13 @@
    1.14    "ADDTESTS/course/phst11/T3_MathEngine"
    1.15    "ADDTESTS/file-depend/BuildC_Test"
    1.16    "ADDTESTS/course/SignalProcess/Build_Inverse_Z_Transform"
    1.17 -  "../../Pure/Isar/Test_Parsers"
    1.18 -(*"../../Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
    1.19 -  "../../Pure/Isar/Test_Parse_Term"
    1.20 +  "~~/test/Pure/Isar/Test_Parsers"
    1.21 +(*"~~/test/Pure/Isar/Pure/Isar/Struct_Deriv" update 2009-2-->2011*)
    1.22 +  "~~/test/Pure/Isar/Test_Parse_Term"
    1.23 +  "~~/test/HOL/Library/Test_Polynomial"
    1.24 +
    1.25 +  "~~/src/Tools/isac/Knowledge/GCD_Poly"    (*not imported by Isac.thy*)
    1.26 +  "~~/src/Tools/isac/Knowledge/GCD_Poly_FP" (*not imported by Isac.thy*)
    1.27  
    1.28  begin
    1.29  section {* test ML Code of isac *}
    1.30 @@ -127,6 +134,8 @@
    1.31    ML_file "Knowledge/algein.sml"
    1.32    ML_file "Knowledge/diophanteq.sml"
    1.33    ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
    1.34 +  ML_file "Knowledge/gcd_poly_ml.sml"
    1.35 +  ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
    1.36    ML_file "Knowledge/isac.sml"
    1.37    ML_file "Knowledge/build_thydata.sml"
    1.38    ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}