test/Tools/isac/Knowledge/logexp.sml
changeset 59997 46fe5a8c3911
parent 59983 f1fdb213717b
child 60230 0ca0f9363ad3
     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'))];