1.1 --- a/test/Tools/isac/Knowledge/algein.sml Fri Apr 10 16:16:09 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/algein.sml Fri Apr 10 18:32:36 2020 +0200
1.3 @@ -94,7 +94,7 @@
1.4 moveActiveRoot 1;
1.5 autoCalculate 1 CompleteCalc;
1.6 val ((pt,p),_) = get_calc 1; show_pt pt;
1.7 -if p = ([], Res) andalso UnparseC.term2str (get_obj g_res pt (fst p)) = "L = 104" then()
1.8 +if p = ([], Res) andalso UnparseC.term (get_obj g_res pt (fst p)) = "L = 104" then()
1.9 else error "algein.sml: 'Berechnung' 'erstSymbolisch' changed";
1.10
1.11 "----------- Widerspruch 3 = 777 ---------------------------------";
1.12 @@ -106,17 +106,17 @@
1.13 val thm = assoc_thm' thy ("sym_mult_zero_right","");
1.14 val t = str2term "0 = (0::real)";
1.15 val SOME (t',_) = rewrite_ thy rew_ord erls false thm t;
1.16 -UnparseC.term2str t' = "0 = ?a1 * 0"; (* = true*)
1.17 +UnparseC.term t' = "0 = ?a1 * 0"; (* = true*)
1.18
1.19 (*testing code in ME/appl.sml*)
1.20 val sube = ["?a1 = (3::real)"];
1.21 val subte = sube2subte sube;
1.22 -UnparseC.terms2str' subte = "[?a1 = 3]"; (* = true*)
1.23 +UnparseC.terms_short subte = "[?a1 = 3]"; (* = true*)
1.24 val subst = sube2subst thy sube;
1.25 foldl and_ (true, map contains_Var subte);
1.26
1.27 val t'' = subst_atomic subst t';
1.28 -UnparseC.term2str t'' = "0 = 3 * 0"; (* = true*)
1.29 +UnparseC.term t'' = "0 = 3 * 0"; (* = true*)
1.30
1.31 val thm = assoc_thm' thy ("sym","");
1.32 (*----- STOPPED.WN0x?: Widerspruch 3 = 777: sym contains "==>" instead of "=" !!!