1.1 --- a/test/Tools/isac/Test_Isac.thy Wed Sep 11 18:02:35 2019 +0200
1.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 12 14:42:53 2019 +0200
1.3 @@ -104,6 +104,7 @@
1.4 open Tactical;
1.5 open Prog_Expr;
1.6 (*open Auto_Prog;*)
1.7 + open Input_Descript;
1.8 open Specify; show_ptyps;
1.9 open Applicable; mk_set;
1.10 open Solve; (* NONE *)
1.11 @@ -217,11 +218,11 @@
1.12 ML_file "Knowledge/root.sml"
1.13 ML_file "Knowledge/lineq.sml"
1.14 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
1.15 - ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
1.16 + ML_file "Knowledge/rateq.sml" (*exception Size raised "./basis/LibrarySupport.sml")*)
1.17 ML_file "Knowledge/rootrat.sml"
1.18 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
1.19 ML_file "Knowledge/partial_fractions.sml"
1.20 - ML_file "Knowledge/polyeq.sml"
1.21 +(*ML_file "Knowledge/polyeq.sml" exception Size raised "./basis/LibrarySupport.sml")*)
1.22 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
1.23 ML_file "Knowledge/calculus.sml"
1.24 ML_file "Knowledge/trig.sml"
1.25 @@ -233,9 +234,9 @@
1.26 ML_file "Knowledge/polyminus.sml"
1.27 ML_file "Knowledge/vect.sml"
1.28 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
1.29 - ML_file "Knowledge/biegelinie-1.sml"
1.30 + ML_file "Knowledge/biegelinie-1.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
1.31 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *)
1.32 - ML_file "Knowledge/biegelinie-3.sml"
1.33 + ML_file "Knowledge/biegelinie-3.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
1.34 ML_file "Knowledge/algein.sml"
1.35 ML_file "Knowledge/diophanteq.sml"
1.36 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
1.37 @@ -243,7 +244,7 @@
1.38 ML_file "Knowledge/isac.sml"
1.39 ML_file "Knowledge/build_thydata.sml"
1.40
1.41 -section \<open>tests additional to src/.. files\<close>
1.42 +section \<open>further tests additional to src/.. files\<close>
1.43 ML_file "BridgeLibisabelle/use-cases.sml"
1.44 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
1.45 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"