test/Tools/isac/Test_Isac.thy
changeset 59617 5c4230e32124
parent 59603 30cd47104ad7
child 59618 80efccb7e5c1
     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"