1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Thu Aug 05 18:05:28 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri Aug 06 11:13:20 2021 +0200
     1.3 @@ -241,8 +241,6 @@
     1.4      SOME ("10 * g kleiner f = False", _) => ()
     1.5    | _ => error "polyminus.sml: 10 * g kleiner f = False";
     1.6  
     1.7 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
     1.8 -(*TOODOO eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 \<longrightarrow> False*)
     1.9  case eval_kleiner 0 0 (TermC.str2term "(a \<up> 2) kleiner b") 0 of
    1.10      SOME ("a \<up> 2 kleiner b = True", _) => ()
    1.11    | _ => error "polyminus.sml: a \<up> 2 kleiner b = True";
    1.12 @@ -250,7 +248,6 @@
    1.13  case eval_kleiner 0 0 (TermC.str2term "(3*a \<up> 2) kleiner b") 0 of
    1.14      SOME ("3 * a \<up> 2 kleiner b = True", _) => ()
    1.15    | _ => error "polyminus.sml: 3 * a \<up> 2 kleiner b = True";
    1.16 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.17  
    1.18  case eval_kleiner 0 0 (TermC.str2term "(a*b) kleiner c") 0 of
    1.19      SOME ("a * b kleiner c = True", _) => ()
    1.20 @@ -308,14 +305,13 @@
    1.21  if UnparseC.term t = "a + b + c + d" then ()
    1.22  else error "polyminus.sml: ordne_alphabetisch3 a + b + c + d";
    1.23  
    1.24 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    1.25  "======= compile rls for the most complicated terms";
    1.26  val t = TermC.str2term "5*e + 6*f - 8*g - 9 - 7*e - 4*f + 10*g + 12";
    1.27  "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";
    1.28  val SOME (t,_) = rewrite_set_ thy false ordne_alphabetisch t; 
    1.29  if UnparseC.term t = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g"
    1.30  then () else error "polyminus.sml: ordne_alphabetisch finished";
    1.31 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.32 +
    1.33  
    1.34  
    1.35  "----------- build fasse_zusammen --------------------------------";
    1.36 @@ -478,7 +474,7 @@
    1.37  then () else error "polyminus.sml: Probe 11 = 11";
    1.38  Test_Tool.show_pt pt;
    1.39  
    1.40 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    1.41 +
    1.42  "----------- pbl klammer polynom vereinfachen p.34 ---------------";
    1.43  "----------- pbl klammer polynom vereinfachen p.34 ---------------";
    1.44  "----------- pbl klammer polynom vereinfachen p.34 ---------------";
    1.45 @@ -494,7 +490,6 @@
    1.46     UnparseC.term (get_obj g_res pt (fst p)) = "1 + 14 * u"
    1.47  then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
    1.48  Test_Tool.show_pt pt;
    1.49 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.50  
    1.51  "======= probe p.34 -----";
    1.52  reset_states ();
    1.53 @@ -510,7 +505,7 @@
    1.54  then () else error "polyminus.sml: Probe 29 = 29";
    1.55  Test_Tool.show_pt pt;
    1.56  
    1.57 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    1.58 +
    1.59  "----------- try fun applyTactics --------------------------------";
    1.60  "----------- try fun applyTactics --------------------------------";
    1.61  "----------- try fun applyTactics --------------------------------";
    1.62 @@ -572,7 +567,9 @@
    1.63  (([9], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f)),
    1.64  (([], Res), - (8 * g) + 10 * g + (3 - 2 * e + 2 * f))]
    1.65  ~~~~~~~~~~~###~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
    1.66 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.67 +val ([], Res) = p;
    1.68 +val "2 * g + (3 - 2 * e + 2 * f)" = get_obj g_res pt (fst p) |> UnparseC.term;
    1.69 +(* ---------^^^--- not quite perfect*)
    1.70  
    1.71  
    1.72  "#############################################################################";
    1.73 @@ -643,13 +640,10 @@
    1.74  autoCalculate 1 CompleteCalc;
    1.75  val ((pt,p),_) = get_calc 1; Test_Tool.show_pt pt;
    1.76  
    1.77 -UnparseC.term (get_obj g_res pt (fst p)) = "8 * a + 3 * a * 4 * a - 3 * a * 1 - 2";
    1.78 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    1.79  if p = ([], Res) andalso
    1.80     UnparseC.term (get_obj g_res pt (fst p)) =(*"- 2 + 12 * a \<up> 2 + 5 * a" with OLD numerals*)
    1.81                                                 "- 2 + 5 * a + 12 * a \<up> 2"
    1.82  then () else error "polyminus.sml: Vereinfache (2*u - 5 - (3 - ...";
    1.83 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.84  
    1.85  "----------- pbl binom polynom vereinfachen: cube ----------------";
    1.86  "----------- pbl binom polynom vereinfachen: cube ----------------";