1.1 --- a/test/Tools/isac/Test_Isac.thy Sat Aug 24 11:54:39 2013 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Sat Aug 24 17:41:40 2013 +0200
1.3 @@ -110,10 +110,9 @@
1.4 ML_file "Knowledge/atools.sml"
1.5 ML_file "Knowledge/simplify.sml"
1.6 ML_file "Knowledge/poly.sml"
1.7 -(*THIS WAITS UNTIL Isabelle2013 IN THIS SEQUENCE (SEE Test_Some2.thy):0
1.8 - ML_file "Knowledge/gcd_poly.sml" (*type error 'nth' etc*)
1.9 - ML_file "Knowledge/gcd_poly_winkler.sml"*)
1.10 -(*ML_file "Knowledge/rational.sml" WN120317.TODO postponed to joint work with dmeindl *)
1.11 + ML_file "Knowledge/gcd_poly_ml.sml"
1.12 + ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
1.13 + ML_file "Knowledge/rational.sml"
1.14 ML_file "Knowledge/equation.sml"
1.15 ML_file "Knowledge/root.sml"
1.16 ML_file "Knowledge/lineq.sml"
1.17 @@ -138,8 +137,6 @@
1.18 ML_file "Knowledge/algein.sml"
1.19 ML_file "Knowledge/diophanteq.sml"
1.20 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
1.21 - ML_file "Knowledge/gcd_poly_ml.sml"
1.22 - ML_file "Knowledge/gcd_poly_winkler.sml" (*must be after gcd_poly_ml.sml: redefines functions*)
1.23 ML_file "Knowledge/isac.sml"
1.24 ML_file "Knowledge/build_thydata.sml"
1.25 ML {*"%%%%%%%%%%%%%%%%% end Knowledge %%%%%%%%%%%%%%%%%%%%%%%%";*}