1.1 --- a/test/Tools/isac/Knowledge/biegelinie.sml	Wed Feb 14 06:06:27 2018 +0100
     1.2 +++ b/test/Tools/isac/Knowledge/biegelinie.sml	Wed Feb 14 08:05:37 2018 +0100
     1.3 @@ -286,7 +286,7 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
     1.5  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
     1.6  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
     1.7 -if f2str f = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
     1.8 +if f2str f = "[c_2 = 0 / (-1 * EI), L * c + c_2 = -1 * q_0 * L ^^^ 4 / (-24 * EI)]" then ()
     1.9  else error  "biegelinie.sml: Bsp 7.27 #21 f";
    1.10  case nxt of
    1.11      (_, Subproblem
    1.12 @@ -317,10 +317,9 @@
    1.13  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    1.14  val (p,_,f,nxt,_,pt) = me nxt p c pt; f2str f;
    1.15  if f2str f = 
    1.16 -"y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n\
    1.17 - \(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n\
    1.18 - \ -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)" then ()
    1.19 -else error  "biegelinie.sml: Bsp 7.27 #24 f";
    1.20 +  "y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n" ^
    1.21 +  "(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
    1.22 +then () else error  "biegelinie.sml: Bsp 7.27 #24 f";
    1.23  case nxt of ("End_Proof'", End_Proof') => ()
    1.24  	  | _ => error  "biegelinie.sml: Bsp 7.27 #24";
    1.25  
    1.26 @@ -395,7 +394,7 @@
    1.27  val ((pt,p),_) = get_calc 1;
    1.28  if p = ([], Res) andalso length (children pt) = 23 andalso 
    1.29  term2str (get_obj g_res pt (fst p)) = 
    1.30 -"y x =\n-1 * q_0 * L ^^^ 4 / (-24 * EI * L) * x +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
    1.31 +"y x =\n0 / (-1 * EI) +\n(0 / (-1 * EI) / L + -1 * q_0 * L ^^^ 4 / (-24 * EI) / L * x) +\n(2 * L * q_0 / (-1 * 24 * EI) * x ^^^ 3 +\n -1 * q_0 / (-1 * 24 * EI) * x ^^^ 4)"
    1.32  then () else error "biegelinie.sml: 1st biegelin.7.27 changed";
    1.33  
    1.34   val (unc, del, gen) = (([],Pbl), ([],Pbl), ([],Res));

     2.1 --- a/test/Tools/isac/Knowledge/eqsystem.sml	Wed Feb 14 06:06:27 2018 +0100
     2.2 +++ b/test/Tools/isac/Knowledge/eqsystem.sml	Wed Feb 14 08:05:37 2018 +0100
     2.3 @@ -179,19 +179,19 @@
     2.4  	    \ 0 = c_2 + c * L + 1 / EI * (L * q_0 / 12 * L ^^^ 3 +         \
     2.5  	    \                                     -1 * q_0 / 24 * L ^^^ 4)]";
     2.6  val SOME (t,_) = rewrite_set_ thy true norm_Rational t;
     2.7 -if term2str t="[0 = c_2, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"
     2.8 +if term2str t="[0 = c_2 + 0 / EI, 0 = c_2 + L * c + L ^^^ 4 * q_0 / (EI * 24)]"
     2.9  then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.0b";
    2.10  
    2.11  val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System_parenthesized t;
    2.12 -if term2str t = "[0 = c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
    2.13 +if term2str t = "[0 = 0 / EI + c_2, 0 = q_0 * L ^^^ 4 / (24 * EI) + (L * c + c_2)]"
    2.14  then () else error "eqsystem.sml rewrite in 2x2 simplify_System_par.1b";
    2.15  
    2.16  val SOME (t,_) = rewrite_set_inst_ thy true bdvs isolate_bdvs t;
    2.17 -if term2str t = "[c_2 = 0, L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
    2.18 +if term2str t = "[c_2 = 0 + -1 * (0 / EI),\n L * c + c_2 = 0 + -1 * (q_0 * L ^^^ 4 / (24 * EI))]"
    2.19  then () else error "eqsystem.sml rewrite in 2x2 isolate_bdvs b";
    2.20  
    2.21  val SOME(t,_)= rewrite_set_inst_ thy true bdvs simplify_System t;
    2.22 -if term2str t = "[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
    2.23 +if term2str t = "[c_2 = 0 / EI, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
    2.24  then () else error "eqsystem.sml rewrite in 2x2 simplify_System.2b";
    2.25  
    2.26  val xxx = rewrite_set_ thy true order_system t;
    2.27 @@ -594,7 +594,7 @@
    2.28  val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
    2.29  val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
    2.30  if f2str f = 
    2.31 -"[c_2 = 0, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
    2.32 +"[c_2 = 0 / EI, L * c + c_2 = -1 * q_0 * L ^^^ 4 / (24 * EI)]"
    2.33  then () else error "eqsystem.sml me simpl. before SubProblem b";
    2.34  case nxt of
    2.35      (_, Subproblem ("Biegelinie", ["triangular", "2x2", "LINEAR",_])) => ()
    2.36 @@ -630,7 +630,7 @@
    2.37  val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
    2.38  val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f;
    2.39  if f2str f = 
    2.40 -"[c = -1 * q_0 * L ^^^ 4 / (24 * EI * L), c_2 = 0]"
    2.41 +"[c = (0 / EI + -1 * q_0 * L ^^^ 4 / (24 * EI)) / L, c_2 = 0 / EI]"
    2.42  then () else error "eqsystem.sml me [EqSys...2x2] finished f2str f b";
    2.43  case nxt of
    2.44      (_, End_Proof') => ()

     3.1 --- a/test/Tools/isac/Knowledge/integrate.sml	Wed Feb 14 06:06:27 2018 +0100
     3.2 +++ b/test/Tools/isac/Knowledge/integrate.sml	Wed Feb 14 08:05:37 2018 +0100
     3.3 @@ -428,7 +428,7 @@
     3.4  Iterator 1;
     3.5  moveActiveRoot 1;
     3.6  autoCalculate 1 CompleteCalc;
     3.7 -val ((pt,p),_) = get_calc 1; PolyML.makestring p; show_pt pt;
     3.8 +val ((pt,p),_) = get_calc 1; @{make_string} p; show_pt pt;
     3.9  val (Form t,_,_) = pt_extract (pt, p); 
    3.10  if term2str t = "c + x + 1 / 3 * x ^^^ 3" then ()
    3.11  else error "integrate.sml -- interSteps [diff,integration] -- result";

     4.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Wed Feb 14 06:06:27 2018 +0100
     4.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Wed Feb 14 08:05:37 2018 +0100
     4.3 @@ -244,13 +244,21 @@
     4.4  
     4.5  val (Form f, tac, asms) = pt_extract (pt, p);
     4.6  if term2str f = "4 / (z - 1 / 2) + -4 / (z - -1 / 4)" andalso
     4.7 -  terms2str' asms = "[~ matches (?a = 0) (3 = -3 * B / 4) | ~ lhs (3 = -3 * B / 4) is_poly_in B," ^
     4.8 -  "B = -4,lhs (3 + 3 / 4 * B = 0) is_poly_in B,lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^
     4.9 -  "B is_polyexp,A is_polyexp," ^
    4.10 -  "<not> matches (?a = 0) (3 = 3 * A / 4) | <not> lhs (3 = 3 * A / 4) is_poly_in A," ^
    4.11 -  "A = 4,lhs (3 + -3 / 4 * A = 0) is_poly_in A,lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^
    4.12 -  "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
    4.13 -  "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z,z = 1 / 2,z = -1 / 4,z is_polyexp]"
    4.14 +  terms2str' asms = "[\<not> matches (?a = 0) (3 = -3 * B / 4) \<or>\n" ^
    4.15 +    "\<not> lhs (3 = -3 * B / 4) is_poly_in B,B = -4," ^
    4.16 +    "lhs (3 + 3 / 4 * B = 0) is_poly_in B," ^
    4.17 +    "lhs (3 + 3 / 4 * B = 0) has_degree_in B = 1," ^
    4.18 +    "B is_polyexp," ^
    4.19 +    "A is_polyexp," ^
    4.20 +    "\<not> matches (?a = 0) (3 = 3 * A / 4) \<or>\n\<not> lhs (3 = 3 * A / 4) is_poly_in A," ^
    4.21 +    "A = 4," ^
    4.22 +    "lhs (3 + -3 / 4 * A = 0) is_poly_in A," ^
    4.23 +    "lhs (3 + -3 / 4 * A = 0) has_degree_in A = 1," ^
    4.24 +    "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) has_degree_in z = 2," ^
    4.25 +    "lhs (-1 + -2 * z + 8 * z ^^^ 2 = 0) is_poly_in z," ^
    4.26 +    "z = 1 / 2," ^
    4.27 +    "z = -1 / 4," ^
    4.28 +    "z is_polyexp]"
    4.29  then case tac of NONE => ()
    4.30    | _ => error "autoCalculate for met_partial_fraction changed: final result 1"
    4.31  else error "autoCalculate for met_partial_fraction changed: final result 2"

     5.1 --- a/test/Tools/isac/Knowledge/polyeq.sml	Wed Feb 14 06:06:27 2018 +0100
     5.2 +++ b/test/Tools/isac/Knowledge/polyeq.sml	Wed Feb 14 08:05:37 2018 +0100
     5.3 @@ -821,9 +821,9 @@
     5.4  
     5.5  val rls = calculate_RootRat;
     5.6  val SOME (t,asm) = rewrite_set_ thy true rls t;
     5.7 -if term2str t = 
     5.8 -"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
     5.9 -(*"-1 * x = -1 + sqrt (1 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (1 ^^^ 2 - -8))"*)
    5.10 +if term2str t =
    5.11 +  "-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) \<or>\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"
    5.12 +(*"-1 * x = -1 + sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8) |\nx = -1 * -1 + -1 * (-1 * sqrt (2 ^^^ 2 / 2 ^^^ 2 - -8))"..isabisac15*)
    5.13  then () else error "(-8 - 2*x + x^^^2 = 0),  by rewriting -- ERROR INDICATES IMPROVEMENT";
    5.14  (*SHOULD BE: term2str = "x = -2 | x = 4;*)
    5.15  
    5.16 @@ -1158,7 +1158,5 @@
    5.17  (* NONE with d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=0))"
    5.18     instead   d2_reduce_equation1:   "(bdv*(a +b*bdv)=0) = ((bdv=0)|(a+b*bdv=(0::real)))"
    5.19  *)
    5.20 -if term2str t'' = "x = 0 | -6 + 5 * x = 0" then ()
    5.21 +if term2str t'' = "x = 0 \<or> -6 + 5 * x = 0" then ()
    5.22  else error "rls d2_polyeq_bdv_only_simplify broken";
    5.23 -
    5.24 -

     6.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Feb 14 06:06:27 2018 +0100
     6.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Wed Feb 14 08:05:37 2018 +0100
     6.3 @@ -605,7 +605,10 @@
     6.4  if term2str t = "~ (matchsub ((?a::real) + ((?b::real) + (?c::real))) (t_t::real) |\n   matchsub (?a + (?b - ?c)) t_t |\n   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
     6.5  then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
     6.6  show_types := false;*)
     6.7 -if term2str t = "<not> (matchsub (?a + (?b + ?c)) t_t |\n   matchsub (?a + (?b - ?c)) t_t |\n" ^
     6.8 -"   matchsub (?a - (?b + ?c)) t_t | matchsub (?a + (?b - ?c)) t_t)"
     6.9 +if term2str t =
    6.10 +  "\<not> (matchsub (?a + (?b + ?c)) t_t \<or>\n        " ^
    6.11 +  "matchsub (?a + (?b - ?c)) t_t \<or>\n        " ^
    6.12 +  "matchsub (?a - (?b + ?c)) t_t \<or> " ^
    6.13 +  "matchsub (?a + (?b - ?c)) t_t)"
    6.14  then () else error "polyminus.sml type-structure of \"?a :: real\" changed 1";
    6.15