1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Wed Aug 04 17:34:47 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Thu Aug 05 18:05:28 2021 +0200
     1.3 @@ -35,19 +35,16 @@
     1.4  "----------- fun identifier --------------------------------------------------------------------";
     1.5  "----------- fun identifier --------------------------------------------------------------------";
     1.6  "----------- fun identifier --------------------------------------------------------------------";
     1.7 -(*+*)identifier (TermC.str2term "12 ::real") = "|||||||||||||";
     1.8 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
     1.9  if identifier (TermC.str2term "12 ::real") = "12"     then () else error "identifier 1";
    1.10 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.11 +if identifier (TermC.str2term
    1.12 +  "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g ::real") = "|||||||||||||"
    1.13 +                                                      then () else error "identifier 1a";
    1.14  
    1.15  if identifier (TermC.str2term "a ::real") = "a"       then () else error "identifier 2";
    1.16  if identifier (TermC.str2term "3 * a ::real") = "a"   then () else error "identifier 3";
    1.17  
    1.18 -(*+*)identifier (TermC.str2term "a \<up> 2 ::real") = "|||||||||||||";(*TOODOO <-- START HERE*)
    1.19 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    1.20  if identifier (TermC.str2term "a \<up> 2 ::real") = "a"   then () else error "identifier 4";
    1.21  if identifier (TermC.str2term "3*a \<up> 2 ::real") = "a" then () else error "identifier 5";
    1.22 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.23  if identifier (TermC.str2term "a * b ::real") = "b"   then () else error "identifier 5b";
    1.24  
    1.25  (*these are strange (see "specific monomials" in comment to fun.def.)..*)
    1.26 @@ -67,8 +64,6 @@
    1.27  TermC.str2term "aaa";
    1.28  TermC.str2term "222 * aaa";
    1.29  
    1.30 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    1.31 -(*TOODOO eval_kleiner *)
    1.32  case eval_kleiner 0 0 (TermC.str2term "123 kleiner 32") 0 of
    1.33      SOME ("123 kleiner 32 = False", _) => ()
    1.34    | _ => error "polyminus.sml: 12 kleiner 9 = False";
    1.35 @@ -95,7 +90,7 @@
    1.36  val t = TermC.str2term "12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * (g::real)";
    1.37  val SOME ("12 kleiner 5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g = True", _) =
    1.38             eval_kleiner "aaa" "bbb" t "ccc";
    1.39 -"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>",_) $ a $ b)), _) =
    1.40 +"~~~~~ fun eval_kleiner , args:"; val (_, _, (p as (Const (\<^const_name>\<open>kleiner\<close>,_) $ a $ b)), _) =
    1.41    ("aaa", "bbb", t, "ccc");
    1.42      (*if*) TermC.is_num b (*else*);
    1.43  
    1.44 @@ -105,7 +100,6 @@
    1.45    Const (\<^const_name>\<open>numeral\<close>, _) $ (Const (\<^const_name>\<open>num.Bit0\<close>, _) $
    1.46      (Const (\<^const_name>\<open>num.Bit0\<close>, _) $ (Const (\<^const_name>\<open>num.Bit1\<close>, _) $ Const (\<^const_name>\<open>num.One\<close>, _)))) => ()
    1.47  | _ => error "eval_kleiner CHANGED";                                                 (*isa*)
    1.48 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.49  
    1.50  
    1.51  "----------- fun ist_monom ---------------------------------------------------------------------";
    1.52 @@ -372,20 +366,11 @@
    1.53  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.54  
    1.55  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.56 -   f2str f = "5 * e + 6 * f - 8 * g - 9 - 7 * e - 4 * f + 10 * g + 12";      (*isa == isa2*)
    1.57 -val (p''''',_,f,nxt''''',_,pt''''') = me nxt p c pt;
    1.58 -   val                 Check_Postcond ["plus_minus", "polynom", "vereinfachen"] = nxt;
    1.59 -nxt;
    1.60 -(** )//-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------\\( ** )
    1.61 -   val                              (*TOODOO*) Rewrite_Set "ordne_alphabetisch" = nxt;
    1.62 -   f2str f = "- 9 + 12 + 5 * e - 7 * e + 6 * f - 4 * f - 8 * g + 10 * g";    (*isa2*)
    1.63 -val (p,_,f,nxt,_,pt) = me nxt''''' p''''' c pt''''';
    1.64 -   f2str f = "3 + - 2 * e + 2 * f + 2 * g";                                  (*isa2*)
    1.65  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.66 -   f2str f = "3 - 2 * e + 2 * f + 2 * g";                                    (*isa2*)
    1.67  val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.68 -   f2str f = "3 - 2 * e + 2 * f + 2 * g";                                    (*isa2*)
    1.69 -if f2str f = "3 - 2 * e + 2 * f + 2 * g"                                     (*isa2*)
    1.70 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.71 +val (p,_,f,nxt,_,pt) = me nxt p c pt;
    1.72 +if f2str f = "3 - 2 * e + 2 * f + 2 * g" 
    1.73  then case nxt of End_Proof' => () | _ =>  error "me simplification.for_polynomials.with_minus 1"
    1.74  else error "polyminus.sml: me simplification.for_polynomials.with_minus 2";
    1.75  
    1.76 @@ -417,7 +402,6 @@
    1.77  if p = ([], Res) andalso 
    1.78     UnparseC.term (get_obj g_res pt (fst p)) = "3 + 3 * r + 6 * s - 8 * t"
    1.79  then () else error "polyminus.sml: Vereinfache 140 d)";
    1.80 -( ** )\\-----------TOODOO broken with merge after "eliminate ThmC.numerals_to_Free"--------//( **)
    1.81  
    1.82  "======= 139 c ---";
    1.83  reset_states ();