1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Mon Apr 19 20:44:18 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Tue Apr 20 16:58:44 2021 +0200
     1.3 @@ -45,13 +45,13 @@
     1.4      SOME ("3 * a ist_monom = True", _) => ()
     1.5    | _ => error "polyminus.sml: 3 * a ist_monom = True";
     1.6  
     1.7 -case eval_ist_monom 0 0 (TermC.str2term "(a^^^2) ist_monom") 0 of 
     1.8 -   SOME ("a ^^^ 2 ist_monom = True", _) => ()
     1.9 -  | _ => error "polyminus.sml: a^^^2 ist_monom = True";
    1.10 +case eval_ist_monom 0 0 (TermC.str2term "(a \<up> 2) ist_monom") 0 of 
    1.11 +   SOME ("a \<up> 2 ist_monom = True", _) => ()
    1.12 +  | _ => error "polyminus.sml: a \<up> 2 ist_monom = True";
    1.13  
    1.14 -case eval_ist_monom 0 0 (TermC.str2term "(3*a^^^2) ist_monom") 0 of
    1.15 -    SOME ("3 * a ^^^ 2 ist_monom = True", _) => ()
    1.16 -  | _ => error "polyminus.sml: 3*a^^^2 ist_monom = True";
    1.17 +case eval_ist_monom 0 0 (TermC.str2term "(3*a \<up> 2) ist_monom") 0 of
    1.18 +    SOME ("3 * a \<up> 2 ist_monom = True", _) => ()
    1.19 +  | _ => error "polyminus.sml: 3*a \<up> 2 ist_monom = True";
    1.20  
    1.21  case eval_ist_monom 0 0 (TermC.str2term "(a*b) ist_monom") 0 of
    1.22      SOME ("a * b ist_monom = True", _) => ()
    1.23 @@ -139,13 +139,13 @@
    1.24      SOME ("10 * g kleiner f = False", _) => ()
    1.25    | _ => error "polyminus.sml: 10 * g kleiner f = False";
    1.26  
    1.27 -case eval_kleiner 0 0 (TermC.str2term "(a^^^2) kleiner b") 0 of
    1.28 -    SOME ("a ^^^ 2 kleiner b = True", _) => ()
    1.29 -  | _ => error "polyminus.sml: a ^^^ 2 kleiner b = True";
    1.30 +case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
    1.31 +    SOME ("a \<up> 2 kleiner b = True", _) => ()
    1.32 +  | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
    1.33  
    1.34 -case eval_kleiner 0 0 (TermC.str2term "(3*a^^^2) kleiner b") 0 of
    1.35 -    SOME ("3 * a ^^^ 2 kleiner b = True", _) => ()
    1.36 -  | _ => error "polyminus.sml: 3 * a ^^^ 2 kleiner b = True";
    1.37 +case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
    1.38 +    SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
    1.39 +  | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
    1.40  
    1.41  case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
    1.42      SOME ("a * b kleiner c = True", _) => ()
    1.43 @@ -414,12 +414,12 @@
    1.44  autoCalculate 1 (Steps 1);
    1.45  autoCalculate 1 (Steps 1);
    1.46  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.47 -"----- 1 ^^^";
    1.48 +"----- 1  \<up> ";
    1.49  fetchApplicableTactics 1 0 p;
    1.50  val appltacs = specific_from_prog pt p;
    1.51  applyTactic 1 p (hd appltacs) (*addiere_x_plus_minus*);
    1.52  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.53 -"----- 2 ^^^";
    1.54 +"----- 2  \<up> ";
    1.55  (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
    1.56  val erls = erls_ordne_alphabetisch;
    1.57  val t = TermC.str2term "- 9 + 12 + 5 * e - 7 * e + (6 - 4) * f - 8 * g + 10 * g";
    1.58 @@ -440,21 +440,21 @@
    1.59  
    1.60  applyTactic 1 p (hd (specific_from_prog pt p)) (*tausche_minus*);
    1.61  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.62 -"----- 3 ^^^";
    1.63 +"----- 3  \<up> ";
    1.64  applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.65  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.66 -"----- 4 ^^^";
    1.67 +"----- 4  \<up> ";
    1.68  applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.69  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.70 -"----- 5 ^^^";
    1.71 +"----- 5  \<up> ";
    1.72  applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.73  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.74 -"----- 6 ^^^";
    1.75 +"----- 6  \<up> ";
    1.76  
    1.77  (*<CALCMESSAGE> failure </CALCMESSAGE>
    1.78  applyTactic 1 p (hd (specific_from_prog pt p)) (**);
    1.79  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.80 -"----- 7 ^^^";
    1.81 +"----- 7  \<up> ";
    1.82  *)
    1.83  autoCalculate 1 CompleteCalc;
    1.84  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.85 @@ -531,7 +531,7 @@
    1.86  autoCalculate 1 CompleteCalc;
    1.87  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.88  if p = ([], Res) andalso 
    1.89 -   UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a ^^^ 2 + 5 * a"
    1.90 +   UnparseC.term (get_obj g_res pt (fst p)) = "-2 + 12 * a \<up> 2 + 5 * a"
    1.91  then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
    1.92  
    1.93  "----------- pbl binom polynom vereinfachen: cube ----------------";