test/Tools/isac/Test_Isac.thy
changeset 59372 749a56702a67
parent 59370 b829919afd7b
child 59373 bbb414976dfe
     1.1 --- a/test/Tools/isac/Test_Isac.thy	Wed Feb 14 08:05:37 2018 +0100
     1.2 +++ b/test/Tools/isac/Test_Isac.thy	Wed Feb 14 10:50:12 2018 +0100
     1.3 @@ -104,8 +104,6 @@
     1.4    open Model;                  (* NONE *)
     1.5  (*\--- ! aktivate for Test_Isac END ----------------------------------------------------------/*)
     1.6  *}
     1.7 -(*---------------------- check test file by testfile -------------------------------------------
     1.8 -  ---------------------- check test file by testfile -------------------------------------------*)
     1.9  
    1.10  ML {*
    1.11  "~~~~~ fun xxx, args:"; val () = ();
    1.12 @@ -118,6 +116,8 @@
    1.13    (*fun autoCalculate' cI auto = autoCalculate cI auto (*|> Future.join*)*);
    1.14  *}
    1.15  
    1.16 +(*---------------------- check test file by testfile -------------------------------------------
    1.17 +  ---------------------- check test file by testfile -------------------------------------------*)
    1.18  section {* trials with Isabelle's functions *}
    1.19    ML {*"%%%%%%%%%%%%%%%%% start Isabelle %%%%%%%%%%%%%%%%%%%%%%%";*}
    1.20    ML_file "~~/test/Pure/General/alist.ML"
    1.21 @@ -204,16 +204,7 @@
    1.22  (*ML_file "Knowledge/rooteq.sml"    some complicated equations not recovered from 2002 *)
    1.23    ML_file "Knowledge/rateq.sml"   (*some complicated equations not recovered from 2002 *)
    1.24    ML_file "Knowledge/rootrat.sml"
    1.25 -
    1.26 -ML {*
    1.27 -"~~~~~ fun xxx, args:"; val () = ();
    1.28 -*} ML {*
    1.29 -
    1.30 -*} ML {*
    1.31 -*}
    1.32 -
    1.33    ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
    1.34 -(*---------------------- check test file by testfile -------------------------------------------
    1.35    ML_file "Knowledge/partial_fractions.sml"
    1.36    ML_file "Knowledge/polyeq.sml"
    1.37  (*ML_file "Knowledge/rlang.sml"     much to clean up, similar tests in other files     *)
    1.38 @@ -227,7 +218,8 @@
    1.39    ML_file "Knowledge/polyminus.sml"
    1.40    ML_file "Knowledge/vect.sml"
    1.41    ML_file "Knowledge/diffapp.sml"        (* postponed to dev. specification | TP-prog. *)
    1.42 -  ML_file "Knowledge/biegelinie.sml"
    1.43 +  ML_file "Knowledge/biegelinie-1.sml"
    1.44 +(*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: exception Size raised *)
    1.45    ML_file "Knowledge/algein.sml"
    1.46    ML_file "Knowledge/diophanteq.sml"
    1.47    ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
    1.48 @@ -239,7 +231,6 @@
    1.49    ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
    1.50    ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
    1.51    ML {*"%%%%%%%%%%%%%%%%% end ADDTESTS %%%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.52 -  ---------------------- check test file by testfile -------------------------------------------*)
    1.53  
    1.54    ML {*"%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%";*}
    1.55    ML {*"%%%%%%%%%%%%%%%%% end Test_Isac %%%%%%%%%%%%%%%%%%%%%%%%";*}