1.1 --- a/test/Tools/isac/Interpret/lucas-interpreter.sml	Thu Aug 05 18:05:28 2021 +0200
     1.2 +++ b/test/Tools/isac/Interpret/lucas-interpreter.sml	Fri Aug 06 11:13:20 2021 +0200
     1.3 @@ -262,14 +262,14 @@
     1.4    then () else error "specific_from_prog ([1], Res) 1 CHANGED";  (*GOON*)
     1.5  (*[2], Res*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
     1.6  
     1.7 -(*+*)if map Tactic.input_to_string (specific_from_prog pt p) =
     1.8 -   ["Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")", "Rewrite (\"tausche_plus_minus\", \"?b kleiner ?c \<Longrightarrow> ?a + ?c - ?b = ?a - ?b + ?c\")",
     1.9 -    "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
    1.10 -    "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")", 
    1.11 -(*this is new since ThmC.numerals_to_Free.-----\\*)
    1.12 -    "Calculate PLUS", 
    1.13 -(*this is new since ThmC.numerals_to_Free.-----//*)
    1.14 -    "Calculate MINUS"]
    1.15 +(*+*)if map Tactic.input_to_string (specific_from_prog pt p) = [
    1.16 +  "Rewrite (\"tausche_minus\", \"\<lbrakk>?b ist_monom; ?a kleiner ?b\<rbrakk>\n\<Longrightarrow> ?b - ?a = - ?a + ?b\")",
    1.17 +  "Rewrite (\"subtrahiere_x_plus_minus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x + ?m * ?v - ?l * ?v = ?x + (?m - ?l) * ?v\")",
    1.18 +  "Rewrite (\"subtrahiere_x_minus_plus\", \"\<lbrakk>?l is_const; ?m is_const\<rbrakk>\n\<Longrightarrow> ?x - ?m * ?v + ?l * ?v = ?x + (- ?m + ?l) * ?v\")",
    1.19 +  (*this is new since ThmC.numerals_to_Free.-----\\*)
    1.20 +  "Calculate PLUS",
    1.21 +  (*this is new since ThmC.numerals_to_Free.-----//*)
    1.22 +  "Calculate MINUS"]
    1.23    then () else error "specific_from_prog ([1], Res) 2 CHANGED";
    1.24  (* = ([3], Res)*)val ("ok", (_, _, ptp as (pt, p))) = Step.by_tactic (hd (specific_from_prog pt p)) (pt, p);
    1.25  

     2.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Thu Aug 05 18:05:28 2021 +0200
     2.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri Aug 06 11:13:20 2021 +0200
     2.3 @@ -241,8 +241,6 @@
     2.4      SOME ("10 * g kleiner f = False", _) => ()
     2.5    | _ => error "polyminus.sml: 10 * g kleiner f = False";
     2.6  
     2.7 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
     2.8 -(*TOODOO eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 \<longrightarrow> False*)
     2.9  case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
    2.10      SOME ("a \<up> 2 kleiner b = True", _) => ()
    2.11    | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
    2.12 @@ -250,7 +248,6 @@
    2.13  case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
    2.14      SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
    2.15    | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
    2.16 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    2.17  
    2.18  case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
    2.19      SOME ("a * b kleiner c = True", _) => ()
    2.20 @@ -308,14 +305,13 @@
    2.21  if UnparseC.term t = "a + b + c + d" then ()
    2.22  else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
    2.23  
    2.24 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    2.25  "======= compile rls for the most complicated terms";
    2.26  val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
    2.27  "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
    2.28  val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; 
    2.29  if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
    2.30  then () else error "polyminus.sml: ordne_alphabetisch finished";
    2.31 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    2.32 +
    2.33  
    2.34  
    2.35  "----------- build fasse_zusammen --------------------------------";
    2.36 @@ -478,7 +474,7 @@
    2.37  then () else error "polyminus.sml: Probe 11 = 11";
    2.38  Test_Tool.show_pt pt;
    2.39  
    2.40 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    2.41 +
    2.42  "----------- pbl klammer polynom vereinfachen p.34 ---------------";
    2.43  "----------- pbl klammer polynom vereinfachen p.34 ---------------";
    2.44  "----------- pbl klammer polynom vereinfachen p.34 ---------------";
    2.45 @@ -494,7 +490,6 @@
    2.46     UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
    2.47  then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
    2.48  Test_Tool.show_pt pt;
    2.49 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    2.50  
    2.51  "======= probe p.34 -----";
    2.52  reset_states ();
    2.53 @@ -510,7 +505,7 @@
    2.54  then () else error "polyminus.sml: Probe 29 = 29";
    2.55  Test_Tool.show_pt pt;
    2.56  
    2.57 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    2.58 +
    2.59  "----------- try fun applyTactics --------------------------------";
    2.60  "----------- try fun applyTactics --------------------------------";
    2.61  "----------- try fun applyTactics --------------------------------";
    2.62 @@ -572,7 +567,9 @@
    2.63  (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
    2.64  (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
    2.65  ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    2.66 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    2.67 +val ([], Res) = p;
    2.68 +val "2 * g + (3 - 2 * e + 2 * f)" = get_obj g_res pt (fst p) |> UnparseC.term;
    2.69 +(* ---------^^^--- not quite perfect*)
    2.70  
    2.71  
    2.72  "#############################################################################";
    2.73 @@ -643,13 +640,10 @@
    2.74  autoCalculate 1 CompleteCalc;
    2.75  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    2.76  
    2.77 -UnparseC.term (get_obj g_res pt (fst p)) = "8 * a + 3 * a * 4 * a - 3 * a * 1 - 2";
    2.78 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    2.79  if p = ([], Res) andalso
    2.80     UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \<up> 2 + 5 * a" with OLD numerals*)
    2.81                                                 "- 2 + 5 * a + 12 * a \<up> 2"
    2.82  then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
    2.83 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    2.84  
    2.85  "----------- pbl binom polynom vereinfachen: cube ----------------";
    2.86  "----------- pbl binom polynom vereinfachen: cube ----------------";