1.1 --- a/test/Tools/isac/Knowledge/diff.sml Thu Apr 09 12:03:14 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/diff.sml Thu Apr 09 17:13:17 2020 +0200
1.3 @@ -98,14 +98,14 @@
1.4 "--- 6 ---";
1.5 val thm = @{thm "diff_var"};
1.6 val (ct, _) = the (rewrite_inst_ thy tless_true erls_diff true subst thm ct);
1.7 -if term2str ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
1.8 +if UnparseC.term2str ct = "2 * x ^^^ (2 - 1) + 3 * 1 + 0" then ()
1.9 else error "diff.sml diff.behav. in rewrite 1";
1.10 "--- 7 ---";
1.11 "--- 7 ---";
1.12 val rls = Test_simplify;
1.13 val ct = (Thm.term_of o the o (parse thy)) "2 * x ^^^ (2 - 1) + 3 * 1 + 0";
1.14 val (ct, _) = the (rewrite_set_ thy true rls ct);
1.15 -if term2str ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
1.16 +if UnparseC.term2str ct = "3 + 2 * x" then () else error "rewrite_set_ Test_simplify 2 changed";
1.17
1.18 "----------- differentiate: me (*+ tacs input*) ---------";
1.19 "----------- differentiate: me (*+ tacs input*) ---------";
1.20 @@ -226,11 +226,11 @@
1.21 atomty screxp0;
1.22
1.23 val screxp1 = subst_atomic [(f_, f), (v_, v)] screxp0;
1.24 -term2str screxp1;
1.25 +UnparseC.term2str screxp1;
1.26 atomty screxp1;
1.27
1.28 val SOME (f'_,_) = rewrite_set_ (@{theory "Isac_Knowledge"}) false srls_diff screxp1;
1.29 -if term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
1.30 +if UnparseC.term2str f'_= "Take (A' = d_d s (s * (a - s)))" then ()
1.31 else error "diff.sml: diff.behav. in 'primed'";
1.32 atomty f'_;
1.33
1.34 @@ -272,30 +272,30 @@
1.35 val rls = diff_conv;
1.36
1.37 val t = str2term "2/x^^^2";
1.38 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.39 -if term2str t = "2 * x ^^^ -2" then () else error "diff.sml 1/x";
1.40 +val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term2str t;
1.41 +if UnparseC.term2str t = "2 * x ^^^ -2" then () else error "diff.sml 1/x";
1.42
1.43 val t = str2term "sqrt (x^^^3)";
1.44 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.45 -if term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2";
1.46 +val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term2str t;
1.47 +if UnparseC.term2str t = "x ^^^ (3 / 2)" then () else error "diff.sml x^1/2";
1.48
1.49 val t = str2term "2 / sqrt x^^^3";
1.50 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.51 -if term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2";
1.52 +val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term2str t;
1.53 +if UnparseC.term2str t = "2 * x ^^^ (-3 / 2)" then () else error"diff.sml x^-1/2";
1.54 val rls = diff_sym_conv;
1.55
1.56 val t = str2term "2 * x ^^^ -2";
1.57 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.58 -if term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x";
1.59 +val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term2str t;
1.60 +if UnparseC.term2str t = "2 / x ^^^ 2" then () else error "diff.sml sym 1/x";
1.61
1.62
1.63 val t = str2term "x ^^^ (3 / 2)";
1.64 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.65 -if term2str t = "sqrt (x ^^^ 3)" then () else error"diff.sml sym x^1/x";
1.66 +val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term2str t;
1.67 +if UnparseC.term2str t = "sqrt (x ^^^ 3)" then () else error"diff.sml sym x^1/x";
1.68
1.69 val t = str2term "2 * x ^^^ (-3 / 2)";
1.70 -val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; term2str t;
1.71 -if term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x";
1.72 +val SOME (t,_) = rewrite_set_inst_ thy false subs rls t; UnparseC.term2str t;
1.73 +if UnparseC.term2str t ="2 / sqrt (x ^^^ 3)"then()else error"diff.sml sym x^-1/x";
1.74
1.75
1.76 "----------- autoCalculate differentiate_on_R 2/x^2 -----";
1.77 @@ -312,7 +312,7 @@
1.78 moveActiveRoot 1;
1.79 autoCalculate 1 CompleteCalc;
1.80 val ((pt,p),_) = get_calc 1; show_pt pt;
1.81 -if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
1.82 +if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) =
1.83 "1 + 2 * x + -1 / x ^^^ 2 + -4 / x ^^^ 3" then ()
1.84 else error "diff.sml: differentiate_on_R 2/x^2 changed";
1.85
1.86 @@ -331,7 +331,7 @@
1.87 *)
1.88 val ((pt,p),_) = get_calc 1; show_pt pt;
1.89
1.90 -if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) =
1.91 +if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) =
1.92 "8 * x ^^^ 7" then ()
1.93 else error "diff.sml: differentiate_on_R (x^3 * x^5) changed";
1.94
1.95 @@ -354,7 +354,7 @@
1.96 trace_LI := false;
1.97 *)
1.98 val ((pt,p),_) = get_calc 1; show_pt pt;
1.99 -if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
1.100 +if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "8 * x ^^^ 7"
1.101 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1.102
1.103 "--------------------------------------------------------";
1.104 @@ -368,7 +368,7 @@
1.105 moveActiveRoot 1;
1.106 autoCalculate 1 CompleteCalc;
1.107 val ((pt,p),_) = get_calc 1; show_pt pt;
1.108 -if p = ([], Res) andalso term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"
1.109 +if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "15 * x ^^^ 14"
1.110 then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
1.111
1.112 "----------- autoCalculate differentiate_equality -------";