1.1 --- a/test/Tools/isac/Knowledge/logexp.sml Tue May 19 12:33:35 2020 +0200
1.2 +++ b/test/Tools/isac/Knowledge/logexp.sml Wed May 20 12:52:09 2020 +0200
1.3 @@ -25,8 +25,8 @@
1.4 equality_power;
1.5 exp_invers_log;
1.6 (* WN071203 ???... wrong thy ?!? because parsing with (theory "Isac_Knowledge") works ?
1.7 -Refine.refine ["equality ((2 log x) = 3)","solveFor x", "solutions L"]
1.8 - ["equation","test"]; *)
1.9 +Refine.refine ["equality ((2 log x) = 3)", "solveFor x", "solutions L"]
1.10 + ["equation", "test"]; *)
1.11 *)
1.12
1.13 val t = str2term "(2 log x)";
1.14 @@ -35,10 +35,10 @@
1.15 atomty t;
1.16
1.17
1.18 -val fmz = ["equality ((2 log x) = 3)","solveFor x", "solutions L"];
1.19 +val fmz = ["equality ((2 log x) = 3)", "solveFor x", "solutions L"];
1.20 val (dI',pI',mI') =
1.21 - ("Isac_Knowledge",["logarithmic","univariate","equation","test"],
1.22 - ["Test","solve_log"]);
1.23 + ("Isac_Knowledge",["logarithmic", "univariate", "equation", "test"],
1.24 + ["Test", "solve_log"]);
1.25 val p = e_pos'; val c = [];
1.26 (*============ inhibit exn 110726 ==============================================
1.27 val (p,_,f,nxt,_,pt) = CalcTreeTEST [(fmz, (dI',pI',mI'))];