1.1 --- a/src/Tools/isac/BridgeLibisabelle/mathml.sml Wed Sep 11 18:02:35 2019 +0200
1.2 +++ b/src/Tools/isac/BridgeLibisabelle/mathml.sml Thu Sep 12 14:42:53 2019 +0200
1.3 @@ -108,7 +108,7 @@
1.4 (*//---------------------------------- rm libisabelle ---------------------------------------\\* )
1.5 XML.Elem (("TERM", []), [Codec.encode Codec.term t])
1.6 ( *------------------------------------ rm libisabelle -----------------------------------------*)
1.7 - XML.Text ("TERM " ^ Rule.term2str t)
1.8 + XML.Text ("(TERM)\n " ^ Rule.term2str t ^ "\n(/TERM)")
1.9 (*\\---------------------------------- rm libisabelle ---------------------------------------//*)
1.10 ])
1.11
2.1 --- a/src/Tools/isac/Knowledge/Build_Thydata.thy Wed Sep 11 18:02:35 2019 +0200
2.2 +++ b/src/Tools/isac/Knowledge/Build_Thydata.thy Thu Sep 12 14:42:53 2019 +0200
2.3 @@ -115,7 +115,6 @@
2.4 @{thm diff_exp_chain}])]]
2.5 \<close>
2.6
2.7 -(*//--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------\* )
2.8 setup \<open>
2.9 KEStore_Elems.insert_fillpats
2.10 [(["IsacKnowledge", "Diff", "Theorems", "diff_sin_chain"],
2.11 @@ -131,7 +130,6 @@
2.12 TermC.parse_patt @{theory Diff} "d_d ?bdv (sin ?u) = _", "chain-rule-diff-both")]: Celem.fillpat list))
2.13 ]
2.14 \<close>
2.15 -( *\\--------- outcomment "Exception- Size raised" during rm libisabelle ----------------------//*)
2.16
2.17 subsubsection \<open>Error patterns for calculation with rationals\<close>
2.18
3.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Wed Sep 11 18:02:35 2019 +0200
3.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_FP.thy Thu Sep 12 14:42:53 2019 +0200
3.3 @@ -345,7 +345,7 @@
3.4
3.5 function (sequential) dvd_up :: "unipoly \<Rightarrow> unipoly \<Rightarrow> bool" (infixl "%|%" 70) where
3.6 "[d] %|% [p] \<longleftrightarrow> (\<bar>d\<bar> \<le> \<bar>p\<bar>) \<and> (p mod d = 0)" |
3.7 -"ds %|% ps \<longleftrightarrow> (*a hint by FH*)
3.8 +"ds %|% ps \<longleftrightarrow> \<comment> \<open>a hint by FH\<close>
3.9 (let
3.10 ds = drop_tl_zeros ds; ps = drop_tl_zeros ps;
3.11 d000 = (List.replicate (List.length ps - List.length ds) 0) @ ds;
3.12 @@ -570,7 +570,7 @@
3.13 "HENSEL_lifting_up a b d M p =
3.14 (let
3.15 p = p next_prime_not_dvd d;
3.16 - g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (int (d mod p))) mod_up p) p (*see above*)
3.17 + g_p = centr_up (((normalise (mod_up_gcd a b p) p) %* (int (d mod p))) mod_up p) p \<comment> \<open>see above\<close>
3.18 in
3.19 if deg_up g_p = 0 then [1] else
3.20 (let
4.1 --- a/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy Wed Sep 11 18:02:35 2019 +0200
4.2 +++ b/src/Tools/isac/Knowledge/GCD_Poly_OLD.thy Thu Sep 12 14:42:53 2019 +0200
4.3 @@ -39,7 +39,7 @@
4.4 fun pConss :: "int list \<Rightarrow> int poly \<Rightarrow> int poly" where
4.5 "pConss [] p = p" |
4.6 "pConss (x # xs) p = pConss xs (pCons x p)"
4.7 -value "pConss (rev (*!!!*) [1,2,3]) [:0:]" \<comment> \<open>Poly [1, 2, 3]\<close>
4.8 +value "pConss (rev \<comment> \<open>!!!\<close> [1,2,3]) [:0:]" \<comment> \<open>Poly [1, 2, 3]\<close>
4.9 value "pConss [] [:1,2,3:]" \<comment> \<open>Poly [1, 2, 3]\<close>
4.10 value "pConss [0,0] [:1,2,3:]" \<comment> \<open>Poly [0, 0, 1, 2, 3]\<close>
4.11
4.12 @@ -94,11 +94,11 @@
4.13 fun for_quot_regarding :: "int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> int poly \<Rightarrow> nat" where
4.14 "for_quot_regarding p1 p2 p1' quot remd =
4.15 (let
4.16 - zeros = degree p1' - degree remd - 1(*length [q]*);
4.17 + zeros = degree p1' - degree remd - 1\<comment> \<open>length [q]\<close>;
4.18 max_qot_deg = degree p1 - degree p2
4.19 in
4.20 - if zeros + 1(*length [q]*) + degree quot > max_qot_deg (*possible in last step of div*)
4.21 - then max_qot_deg - degree quot - 1(*length [q]*)
4.22 + if zeros + 1 \<comment> \<open>length [q]\<close> + degree quot > max_qot_deg \<comment> \<open>possible in last step of div\<close>
4.23 + then max_qot_deg - degree quot - 1 \<comment> \<open>length [q]\<close>
4.24 else zeros)"
4.25
4.26 (* multiply polynomial p such that it has degree d with d = deg p*)
4.27 @@ -239,9 +239,9 @@
4.28 ##2## remd = smult (int n) p1' - smult q (mult_to_deg (degree p1') p2);
4.29 *)
4.30 value "let
4.31 - n = 7289497600::int(*nat*);
4.32 + n = 7289497600::int \<comment> \<open>nat\<close>;
4.33 p1' = pConss (rev [-1316434, -3708859, -867104, 1525321]) [:0:]
4.34 -in smult ((*int*) n) p1'" \<comment> \<open>the type conversion hangs !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\<close>
4.35 +in smult (\<comment> \<open>int\<close> n) p1'" \<comment> \<open>the type conversion hangs !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!\<close>
4.36 value "let
4.37 q = 111::int;
4.38 p1' = pConss (rev [-1316434, -3708859, -867104, 1525321]) [:0:];
4.39 @@ -265,15 +265,15 @@
4.40 value "let
4.41 zeros = 0::nat;
4.42 q = 4447::int;
4.43 - n = 7289497600::(*nat*)int;
4.44 + n = 7289497600::\<comment> \<open>nat\<close> int;
4.45 quot = [:0::int:]
4.46 -in pConss (replicate zeros 0) (pCons q (smult ((*int*) n) quot))"
4.47 +in pConss (replicate zeros 0) (pCons q (smult (\<comment> \<open>int\<close> n) quot))"
4.48
4.49 (*
4.50 ##5## ns = n * ns
4.51 *)
4.52 value "let
4.53 - n = 7289497600::int(*nat*); (*nat even cannot be initialised !!!!!!!!!!!!!!!!!!!!!!!!!!!!!*)
4.54 + n = 7289497600::int\<comment> \<open>nat\<close>; \<comment> \<open>nat even cannot be initialised !!!!!!!!!!!!!!!!!!!!!!!!!!!!!\<close>
4.55 ns = 1::int
4.56 in n * ns" \<comment> \<open>\<close>
4.57
5.1 --- a/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml Wed Sep 11 18:02:35 2019 +0200
5.2 +++ b/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml Thu Sep 12 14:42:53 2019 +0200
5.3 @@ -156,10 +156,12 @@
5.4 val rules = (*xml_to_bool*) string_to_bool rules
5.5 val out = getFormulaeFromTo calcid from to level rules (* <-------------------- *)
5.6 ;
5.7 +(*//---------------------------------- rm libisabelle ---------------------------------------\\* )
5.8 if xmlstr 0 out =
5.9 "(GETELEMENTSFROMTO)\n. (CALCID)\n. . 1\n. (/CALCID)\n. (FORMHEADS)\n. . (CALCFORMULA)\n. . . (POSITION)\n. . . . (INTLIST)\n. . . . (/INTLIST)\n. . . . (POS)\n. . . . . Pbl\n. . . . (/POS)\n. . . (/POSITION)\n. . . (FORMULA)\n. . . . (ISA)\n. . . . . solve (x + 1 = 2, x)\n. . . . (/ISA)\n. . . . (TERM)\n. . . . . solve (x + 1 = 2, x)\n. . . . (/TERM)\n. . . (/FORMULA)\n. . (/CALCFORMULA)\n. (/FORMHEADS)\n(/GETELEMENTSFROMTO)\n"
5.10 then () else error "test--isac-java--isac-kernel step 4: operation_setup getformulaefromto CHANGED";
5.11 out |> xmlstr 0 |> writeln (*
5.12 +( *\\---------------------------------- rm libisabelle ---------------------------------------//*)
5.13 <GETELEMENTSFROMTO>
5.14 . <CALCID>
5.15 . . 1
6.1 --- a/test/Tools/isac/BridgeLibisabelle/mathml.sml Wed Sep 11 18:02:35 2019 +0200
6.2 +++ b/test/Tools/isac/BridgeLibisabelle/mathml.sml Thu Sep 12 14:42:53 2019 +0200
6.3 @@ -104,7 +104,7 @@
6.4 val term = @{term "aaa + bbb::real"};
6.5 val str = term |> xml_of_term_NEW |> xmlstr 0;
6.6 if str =
6.7 -"(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n. . aaa + bbb\n. (/TERM)\n(/FORMULA)\n"
6.8 +"(FORMULA)\n. (ISA)\n. . aaa + bbb\n. (/ISA)\n. (TERM)\n aaa + bbb\n(/TERM)\n(/FORMULA)\n"
6.9 then () else error "term |> xml_of_term_NEW |> xmlstr ..changed";
6.10 writeln str;
6.11
7.1 --- a/test/Tools/isac/Knowledge/rateq.sml Wed Sep 11 18:02:35 2019 +0200
7.2 +++ b/test/Tools/isac/Knowledge/rateq.sml Thu Sep 12 14:42:53 2019 +0200
7.3 @@ -77,6 +77,7 @@
7.4 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.5 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.6 (*val nxt = Apply_Method ["PolyEq", "normalise_poly"])*)
7.7 +(*//---------------------------------- exception Size raised --------------------------------\\* )
7.8 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.9 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.10 (* val nxt = (_,Subproblem ("PolyEq",["polynomial","univariate","equation"]=======*)
7.11 @@ -168,7 +169,8 @@
7.12 if p = ([], Res) andalso f2str f = "[x = 1 / 5]"
7.13 then case nxt of ("End_Proof'", End_Proof') => ()
7.14 | _ => error "rateq.sml: new behaviour: [x = 1 / 5] 1"
7.15 -else error "rateq.sml: new behaviour: [x = 1 / 5] 2"
7.16 +else error "rateq.sml: new behaviour: [x = 1 / 5] 2";
7.17 +( *\\---------------------------------- exception Size raised --------------------------------//*)
7.18
7.19 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
7.20 "------------ S.68, Bsp.: 40, ((x)/(x - 8) + (x - 8)/(x) = 26/5)--";
7.21 @@ -235,7 +237,7 @@
7.22 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.23 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.24 case nxt of ("Apply_Method", Apply_Method ["PolyEq", "normalise_poly"]) => ()
7.25 -| _ => error "55b normalise_poly specification broken";
7.26 +| _ => error "55b normalise_poly specification broken 1";
7.27 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.28 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.29 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.30 @@ -246,7 +248,8 @@
7.31 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.32 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.33 case nxt of ("Apply_Method", Apply_Method ["PolyEq", "solve_d2_polyeq_bdvonly_equation"]) => ()
7.34 -| _ => error "55b normalise_poly specification broken";
7.35 +| _ => error "55b normalise_poly specification broken 2";
7.36 +(*//---------------------------------- exception Size raised --------------------------------\\* )
7.37 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.38 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.39 val (p,_,f,nxt,_,pt) = me nxt p [1] pt; val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.40 @@ -313,13 +316,9 @@
7.41 val (p,_,f,nxt,_,pt) = me nxt p''' [1] pt''';
7.42 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
7.43
7.44 -(*============ inhibit exn WN120316 ==============================================
7.45 -if p = ([], Res) andalso nxt = ("End_Proof'", End_Proof') andalso f2str f = [x = 6 / 5] then ()
7.46 -else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5]";
7.47 -(*WN120317.TODO dropped rateq*)
7.48 -============ inhibit exn WN120316 ==============================================*)
7.49 if p = ([], Res) andalso f2str f = "[]"
7.50 then case nxt of ("End_Proof'", End_Proof') => ()
7.51 | _ => error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 1"
7.52 else error "rlang.sml: diff.behav. in Schalk I s.87 Bsp 55b [x = 6 / 5] 2";
7.53 +( *\\---------------------------------- exception Size raised --------------------------------//*)
7.54
8.1 --- a/test/Tools/isac/Test_Isac.thy Wed Sep 11 18:02:35 2019 +0200
8.2 +++ b/test/Tools/isac/Test_Isac.thy Thu Sep 12 14:42:53 2019 +0200
8.3 @@ -104,6 +104,7 @@
8.4 open Tactical;
8.5 open Prog_Expr;
8.6 (*open Auto_Prog;*)
8.7 + open Input_Descript;
8.8 open Specify; show_ptyps;
8.9 open Applicable; mk_set;
8.10 open Solve; (* NONE *)
8.11 @@ -217,11 +218,11 @@
8.12 ML_file "Knowledge/root.sml"
8.13 ML_file "Knowledge/lineq.sml"
8.14 (*ML_file "Knowledge/rooteq.sml" some complicated equations not recovered from 2002 *)
8.15 - ML_file "Knowledge/rateq.sml" (*some complicated equations not recovered from 2002 *)
8.16 + ML_file "Knowledge/rateq.sml" (*exception Size raised "./basis/LibrarySupport.sml")*)
8.17 ML_file "Knowledge/rootrat.sml"
8.18 ML_file "Knowledge/rootrateq.sml"(*ome complicated equations not recovered from 2002 *)
8.19 ML_file "Knowledge/partial_fractions.sml"
8.20 - ML_file "Knowledge/polyeq.sml"
8.21 +(*ML_file "Knowledge/polyeq.sml" exception Size raised "./basis/LibrarySupport.sml")*)
8.22 (*ML_file "Knowledge/rlang.sml" much to clean up, similar tests in other files *)
8.23 ML_file "Knowledge/calculus.sml"
8.24 ML_file "Knowledge/trig.sml"
8.25 @@ -233,9 +234,9 @@
8.26 ML_file "Knowledge/polyminus.sml"
8.27 ML_file "Knowledge/vect.sml"
8.28 ML_file "Knowledge/diffapp.sml" (* postponed to dev. specification | TP-prog. *)
8.29 - ML_file "Knowledge/biegelinie-1.sml"
8.30 + ML_file "Knowledge/biegelinie-1.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
8.31 (*ML_file "Knowledge/biegelinie-2.sml" since Isabelle2017: "exception Size raised" *)
8.32 - ML_file "Knowledge/biegelinie-3.sml"
8.33 + ML_file "Knowledge/biegelinie-3.sml" (* exception Size raised "./basis/LibrarySupport.sml"*)
8.34 ML_file "Knowledge/algein.sml"
8.35 ML_file "Knowledge/diophanteq.sml"
8.36 ML_file "Knowledge/Inverse_Z_Transform/inverse_z_transform.sml"
8.37 @@ -243,7 +244,7 @@
8.38 ML_file "Knowledge/isac.sml"
8.39 ML_file "Knowledge/build_thydata.sml"
8.40
8.41 -section \<open>tests additional to src/.. files\<close>
8.42 +section \<open>further tests additional to src/.. files\<close>
8.43 ML_file "BridgeLibisabelle/use-cases.sml"
8.44 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
8.45 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"
9.1 --- a/test/Tools/isac/Test_Isac_Short.thy Wed Sep 11 18:02:35 2019 +0200
9.2 +++ b/test/Tools/isac/Test_Isac_Short.thy Thu Sep 12 14:42:53 2019 +0200
9.3 @@ -94,7 +94,7 @@
9.4 open Math_Engine; CalcTreeTEST;
9.5 open Lucin; itms2args;
9.6 open LucinNEW; appy;
9.7 - open Istate;
9.8 + open Istate;
9.9 open Inform; cas_input;
9.10 open Rtools; trtas2str;
9.11 open Chead; pt_extract;
9.12 @@ -189,104 +189,6 @@
9.13 ML_file "Interpret/rewtools.sml"
9.14 ML_file "Interpret/script.sml"
9.15 ML_file "Interpret/inform.sml"
9.16 -ML \<open>
9.17 -\<close> ML \<open>
9.18 -"--------- embed fun find_fillpatterns ---------------------------";
9.19 -"--------- embed fun find_fillpatterns ---------------------------";
9.20 -"--------- embed fun find_fillpatterns ---------------------------";
9.21 -\<close> ML \<open>
9.22 -reset_states ();
9.23 -\<close> ML \<open>
9.24 -CalcTree
9.25 -[(["functionTerm (x ^ 2 + sin (x ^ 4))", "differentiateFor x", "derivative f_f'"],
9.26 - ("Isac_Knowledge", ["derivative_of","function"], ["diff","differentiate_on_R"]))];
9.27 -Iterator 1;
9.28 -moveActiveRoot 1;
9.29 -autoCalculate 1 CompleteCalcHead;
9.30 -autoCalculate 1 (Step 1);
9.31 -autoCalculate 1 (Step 1);(*([1], Res), d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))*)
9.32 -\<close> ML \<open>
9.33 -\<close> ML \<open>
9.34 -appendFormula 1 "d_d x (x ^ 2) + cos (4 * x ^ 3)" (*|> Future.join*);
9.35 - (*<CALCMESSAGE> error pattern #chain-rule-diff-both# </CALCMESSAGE>*)
9.36 - (*or
9.37 - <CALCMESSAGE> no derivation found </CALCMESSAGE>*)
9.38 -\<close> ML \<open>
9.39 -\<close> ML \<open>
9.40 -
9.41 -"~~~~~ fun findFillpatterns, args:"; val (cI, errpatID) = (1, "chain-rule-diff-both");
9.42 - val ((pt, _), _) = get_calc cI
9.43 - val pos = get_pos cI 1;
9.44 -"~~~~~ fun find_fillpatterns, args:"; val ((pt, pos as (p, _)), errpatID) = ((pt, pos), errpatID);
9.45 - val f_curr = get_curr_formula (pt, pos); (* = "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))"*)
9.46 - val pp = par_pblobj pt p
9.47 - val {errpats, scr = Prog prog, ...} = get_met (get_obj g_metID pt pp)
9.48 - val Pstate (env, _, _, _, _, _) = get_istate pt pos
9.49 - val subst = get_bdv_subst prog env
9.50 - val errpatthms = errpats
9.51 - |> filter ((curry op = errpatID) o (#1: errpat -> errpatID))
9.52 - |> map (#3: errpat -> thm list)
9.53 - |> flat;
9.54 -
9.55 -\<close> ML \<open>
9.56 -\<close> ML \<open>
9.57 -map (get_fillpats subst f_curr errpatID) errpatthms |> flat
9.58 -\<close> ML \<open>
9.59 -case map (get_fillpats subst f_curr errpatID) errpatthms |> flat of
9.60 - ("fill-d_d-arg", tm, thm, subs_opt) :: _ => if term2str tm =
9.61 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
9.62 - then () else error "find_fillpatterns changed 1a"
9.63 -| _ => error "find_fillpatterns changed 1b"
9.64 -\<close> ML \<open>
9.65 -
9.66 -"~~~~~ fun get_fillpats, args:"; val (subst, form, errpatID, thm) =
9.67 - (subst, f_curr, errpatID, hd (*simulate beginning of "map"*) errpatthms);
9.68 - val thmDeriv = Thm.get_name_hint thm
9.69 - val (part, thyID) = thy_containing_thm thmDeriv
9.70 - val theID = [part, thyID, "Theorems", thmID_of_derivation_name thmDeriv]
9.71 - val Hthm {fillpats, ...} = get_the theID
9.72 - val some = map (get_fillform subst (thm, form) errpatID) fillpats;
9.73 -
9.74 -case some |> filter is_some |> map the of
9.75 - ("fill-d_d-arg", tm, thm, subsopt) :: _ => if term2str tm =
9.76 - "d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1"
9.77 - then () else error "find_fillpatterns changed 2a"
9.78 -| _ => error "find_fillpatterns changed 2b"
9.79 -
9.80 -"~~~~~ fun get_fillform, args:";
9.81 - val ((subs_opt, subst), (thm, form), errpatID, (fillpatID, pat, erpaID)) =
9.82 - (subst, (thm, form), errpatID, hd (*simulate beginning of "map"*) fillpats);
9.83 -val (form', _, _, rewritten) =
9.84 - rew_sub (Isac()) 1 subst e_rew_ord e_rls false [] (HOLogic.Trueprop $ pat) form;
9.85 -
9.86 -if term2str form' = "d_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" then ()
9.87 -else error "find_fillpatterns changed 3";
9.88 -
9.89 -"~~~~~ to findFillpatterns return val:"; val (fillpats) =
9.90 - (map (get_fillpats (subs_opt, subst) f_curr errpatID) errpatthms |> flat) (*only from "hd errpatthms"*);
9.91 -
9.92 -"vvv--- dropped this code WN120730";
9.93 -val msg = "fill patterns " ^
9.94 - ((map ((apsnd term2str) o quad2pair) fillpats) |> map pair2str_ |> strs2str_);
9.95 -msg =
9.96 - "fill patterns #fill-d_d-arg#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
9.97 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * d_d x ?_dummy_1" ^
9.98 - "#fill-both-args#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
9.99 - " =\nd_d x (x ^^^ 2) + cos ?_dummy_2 * d_d x ?_dummy_3" ^
9.100 - "#fill-d_d#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
9.101 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1 x (x ^^^ 4)" ^
9.102 - "#fill-inner-deriv#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4))" ^
9.103 - " =\nd_d x (x ^^^ 2) + cos (x ^^^ 4) * ?_dummy_1" ^
9.104 - "#fill-all#d_d x (x ^^^ 2) + d_d x (sin (x ^^^ 4)) = d_d x (x ^^^ 2) + ?_dummy_1#";
9.105 -"^^^--- dropped this code WN120730";
9.106 -
9.107 -if (map #1 fillpats) =
9.108 - ["fill-d_d-arg", "fill-both-args", "fill-d_d", "fill-inner-deriv", "fill-all"]
9.109 -then () else error "find_fillpatterns changed 4b";
9.110 -DEconstrCalcTree 1;
9.111 -
9.112 -\<close> ML \<open>
9.113 -\<close>
9.114 ML_file "Interpret/lucas-interpreter.sml"
9.115
9.116 ML_file "MathEngine/solve.sml"
9.117 @@ -341,7 +243,7 @@
9.118 ML_file "Knowledge/isac.sml"
9.119 ML_file "Knowledge/build_thydata.sml"
9.120
9.121 -section \<open>tests additional to src/.. files\<close>
9.122 +section \<open>further tests additional to src/.. files\<close>
9.123 ML_file "BridgeLibisabelle/use-cases.sml"
9.124 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/mini-test.sml"
9.125 ML_file "~~/test/Tools/isac/ADDTESTS/libisabelle/protocol.sml"