1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Aug 02 11:38:40 2021 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Mon Aug 02 15:25:49 2021 +0200
     1.3 @@ -77,7 +77,6 @@
     1.4   if (UnparseC.term t) = "True" then ()
     1.5   else  error "polyeq.sml: diff.behav. 4 in is_expended_in";
     1.6  
     1.7 -
     1.8   val t6 = (Thm.term_of o the o (TermC.parse thy)) "(lhs (-8 - 2*x + x \<up> 2 = 0)) is_expanded_in x";
     1.9   val SOME (t,_) = rewrite_set_ @{theory PolyEq} false PolyEq_prls t6;
    1.10   if (UnparseC.term t) = "True" then ()
    1.11 @@ -112,17 +111,17 @@
    1.12  if M_Match.match_pbl fmz (Problem.from_store ["expanded", "univariate", "equation"]) =
    1.13    M_Match.Matches' {Find = [Correct "solutions L"], 
    1.14              With = [], 
    1.15 -            Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
    1.16 -            Where = [Correct "matches (?a = 0) (-8 - 2 * x + x \<up> 2 = 0)", 
    1.17 -                     Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"], 
    1.18 +            Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
    1.19 +            Where = [Correct "matches (?a = 0) (- 8 - 2 * x + x \<up> 2 = 0)", 
    1.20 +                     Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) is_expanded_in x"], 
    1.21              Relate = []}
    1.22  then () else error "M_Match.match_pbl [expanded,univariate,equation]";
    1.23  
    1.24  if M_Match.match_pbl fmz (Problem.from_store ["degree_2", "expanded", "univariate", "equation"]) =
    1.25    M_Match.Matches' {Find = [Correct "solutions L"], 
    1.26              With = [], 
    1.27 -            Given = [Correct "equality (-8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
    1.28 -            Where = [Correct "lhs (-8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"], 
    1.29 +            Given = [Correct "equality (- 8 - 2 * x + x \<up> 2 = 0)", Correct "solveFor x"], 
    1.30 +            Where = [Correct "lhs (- 8 - 2 * x + x \<up> 2 = 0) has_degree_in x = 2"], 
    1.31              Relate = []}              (*before WN110906 was: has_degree_in x =!= 2"]*)
    1.32  then () else error "M_Match.match_pbl [degree_2,expanded,univariate,equation]";
    1.33  
    1.34 @@ -371,10 +370,10 @@
    1.35  
    1.36  (* und nach dem Re-engineering der Termorders in den 'rulesets' 
    1.37     kannst Du die 'gr"osste' Variable frei w"ahlen: *)
    1.38 -  val bdv= (Thm.term_of o the o (TermC.parse thy)) "''bdv''";
    1.39 -  val x  = (Thm.term_of o the o (TermC.parse thy)) "x";
    1.40 -  val a  = (Thm.term_of o the o (TermC.parse thy)) "a";
    1.41 -  val b  = (Thm.term_of o the o (TermC.parse thy)) "b";
    1.42 +  val bdv= TermC.str2term "bdv ::real";
    1.43 +  val x  = TermC.str2term "x ::real";
    1.44 +  val a  = TermC.str2term "a ::real";
    1.45 +  val b  = TermC.str2term "b ::real";
    1.46  val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,a)] make_polynomial_in x2;
    1.47  if UnparseC.term t' = "b + x + a" then ()
    1.48  else error "termorder.sml diff.behav ord_make_polynomial_in #11";
    1.49 @@ -387,12 +386,8 @@
    1.50  
    1.51    val ppp' = "-6 + -5*x + x \<up> 3 + - 1*x \<up> 2 + - 1*x \<up> 3 + - 14*x \<up> 2";
    1.52    val ppp  = (Thm.term_of o the o (TermC.parse thy)) ppp';
    1.53 -val SOME (t',_) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
    1.54 -if UnparseC.term t' = "- 6 + -5 * x + - 15 * x \<up> 2 + 0" then ()
    1.55 -else error "termorder.sml diff.behav ord_make_polynomial_in #14";
    1.56 -
    1.57  val SOME (t', _) = rewrite_set_inst_ thy false [(bdv,x)] make_polynomial_in ppp;
    1.58 -if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2 + 0" then ()
    1.59 +if UnparseC.term t' = "- 6 + - 5 * x + - 15 * x \<up> 2" then ()
    1.60  else error "termorder.sml diff.behav ord_make_polynomial_in #15";
    1.61  
    1.62    val ttt' = "(3*x + 5)/18 ::real";
    1.63 @@ -401,12 +396,10 @@
    1.64  if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
    1.65  else error "termorder.sml diff.behav ord_make_polynomial_in #16a";
    1.66  
    1.67 -(*============ inhibit exn WN120316 ==============================================
    1.68  val SOME (uuu,_) = rewrite_set_ thy false make_polynomial ttt;
    1.69  if UnparseC.term uuu = "(5 + 3 * x) / 18" then ()
    1.70  else error "termorder.sml diff.behav ord_make_polynomial_in #16b";
    1.71  
    1.72 -
    1.73  "----------- lin.eq degree_0 -------------------------------------";
    1.74  "----------- lin.eq degree_0 -------------------------------------";
    1.75  "----------- lin.eq degree_0 -------------------------------------";