Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
test/Tools/isac/Knowledge/poly-1.sml
changeset 60500 59a3af532717
parent 60424 c3acf9c442ac
child 60509 2e0b7ca391dc
equal deleted inserted replaced
60499:d2407e9cb491 60500:59a3af532717 
   261 
   261 
   262 
   262 
   263 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 
   263 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 
   264 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 
   264 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 
   265 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 
   265 "-------- fun is_addUnordered (x \<up> 2 * y \<up> 2 + x \<up> 3 * y) --------------------------------------";
 
       
   266 val ctxt = Proof_Context.init_global @{theory}
 
   266 val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
 
   267 val t = TermC.str2term "x \<up> 2 * y \<up> 2 + x * x \<up> 2 * y";
 
   267 Rewrite.trace_on := false; (*true false*)
 
   268 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   268 val SOME (t, _) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
       
   269    UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
 
   269    UnparseC.term t = "x \<up> 2 * y \<up> 2 + x \<up> 3 * y";
 
   270 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
 
   270 if UnparseC.term t = "x \<up> 3 * y + x \<up> 2 * y \<up> 2" then ()
 
   271 else error "poly.sml: diff.behav. in make_polynomial 23";
 
   271 else error "poly.sml: diff.behav. in make_polynomial 23";
 
   272 
   272 
   273 (** )
 
   273 (** )
 
   411 "-------- check make_polynomial with simple terms ----------------------------------------------";
 
   411 "-------- check make_polynomial with simple terms ----------------------------------------------";
 
   412 "-------- check make_polynomial with simple terms ----------------------------------------------";
 
   412 "-------- check make_polynomial with simple terms ----------------------------------------------";
 
   413 "-------- check make_polynomial with simple terms ----------------------------------------------";
 
   413 "-------- check make_polynomial with simple terms ----------------------------------------------";
 
   414 "----- check 1 ---";
 
   414 "----- check 1 ---";
 
   415 val t = TermC.str2term "2*3*a";
 
   415 val t = TermC.str2term "2*3*a";
 
   416 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
 
   416 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 
   417 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
 
   417 if UnparseC.term t = "6 * a" then () else error "check make_polynomial 1";
 
   418 
   418 
   419 "----- check 2 ---";
 
   419 "----- check 2 ---";
 
   420 val t = TermC.str2term "2*a + 3*a";
 
   420 val t = TermC.str2term "2*a + 3*a";
 
   421 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
 
   421 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 
   422 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
 
   422 if UnparseC.term t = "5 * a" then () else error "check make_polynomial 2";
 
   423 
   423 
   424 "----- check 3 ---";
 
   424 "----- check 3 ---";
 
   425 val t = TermC.str2term "2*a + 3*a + 3*a";
 
   425 val t = TermC.str2term "2*a + 3*a + 3*a";
 
   426 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
 
   426 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 
   427 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
 
   427 if UnparseC.term t = "8 * a" then () else error "check make_polynomial 3";
 
   428 
   428 
   429 "----- check 4 ---";
 
   429 "----- check 4 ---";
 
   430 val t = TermC.str2term "3*a - 2*a";
 
   430 val t = TermC.str2term "3*a - 2*a";
 
   431 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
 
   431 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 
   432 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
 
   432 if UnparseC.term t = "a" then () else error "check make_polynomial 4";
 
   433 
   433 
   434 "----- check 5 ---";
 
   434 "----- check 5 ---";
 
   435 val t = TermC.str2term "4*(3*a - 2*a)";
 
   435 val t = TermC.str2term "4*(3*a - 2*a)";
 
   436 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
 
   436 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 
   437 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
 
   437 if UnparseC.term t = "4 * a" then () else error "check make_polynomial 5";
 
   438 
   438 
   439 "----- check 6 ---";
 
   439 "----- check 6 ---";
 
   440 val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
 
   440 val t = TermC.str2term "4*(3*a \<up> 2 - 2*a \<up> 2)";
 
   441 val SOME (t, _) = rewrite_set_ thy false make_polynomial t;
 
   441 val SOME (t, _) = rewrite_set_ ctxt false make_polynomial t;
 
   442 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
 
   442 if UnparseC.term t = "4 * a \<up> 2" then () else error "check make_polynomial 6";
 
   443 
   443 
   444 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 
   444 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 
   445 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 
   445 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 
   446 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 
   446 "-------- fun is_multUnordered (x \<up> 2 * x) -----------------------------------------------------";
 
   447 val thy = @{theory "Isac_Knowledge"};
 
   447 val thy = @{theory "Isac_Knowledge"};
 
   448 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
 
   448 "===== works for a simple example, see rewrite.sml -- fun app_rev ===";
 
   449 val t = TermC.str2term "x \<up> 2 * x";
 
   449 val t = TermC.str2term "x \<up> 2 * x";
 
   450 val SOME (t', _) = rewrite_set_ thy true order_mult_ t;
 
   450 val SOME (t', _) = rewrite_set_ ctxt true order_mult_ t;
 
   451 if UnparseC.term t' = "x * x \<up> 2" then ()
 
   451 if UnparseC.term t' = "x * x \<up> 2" then ()
 
   452 else error "poly.sml Poly.is_multUnordered doesn't work";
 
   452 else error "poly.sml Poly.is_multUnordered doesn't work";
 
   453 
   453 
   454 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
 
   454 (* 100928 Rewrite.trace_on shows the first occurring difference in 267b:
 
   455 ###  rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +
 
   455 ###  rls: order_mult_ on: 5 * x \<up> 2 * (2 * x \<up> 7) + 5 * x \<up> 2 * 3 + (6 * x \<up> 7 + 9) + (- 1 * (3 * x \<up> 5 * (6 * x \<up> 4)) + - 1 * (3 * x \<up> 5 * - 1) +
 
   476                           (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 
   476                           (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $ _) $ 
   477                           Const (\<^const_name>\<open>True\<close>, _))) => ()
 
   477                           Const (\<^const_name>\<open>True\<close>, _))) => ()
 
   478   | _ => error "poly.sml diff. eval_is_multUnordered";
 
   478   | _ => error "poly.sml diff. eval_is_multUnordered";
 
   479 
   479 
   480 "----- rewrite_set_ STILL DIDN'T WORK";
 
   480 "----- rewrite_set_ STILL DIDN'T WORK";
 
   481 val SOME (t, _) = rewrite_set_ thy true order_mult_ t;
 
   481 val SOME (t, _) = rewrite_set_ ctxt true order_mult_ t;
 
   482 UnparseC.term t;
 
   482 UnparseC.term t;
 
   483 
   483 
   484 
   484 
   485 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
 
   485 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
 
   486 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
 
   486 "-------- fun is_multUnordered (3 * a + - 2 * a) -----------------------------------------------";
 
   635 
   635 
   636 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 
   636 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 
   637 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 
   637 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 
   638 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 
   638 "-------- fun is_multUnordered  b * a * a ------------------------------------------------------";
 
   639 val t = TermC.str2term "b * a * a";
 
   639 val t = TermC.str2term "b * a * a";
 
   640 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   640 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   641 if UnparseC.term t = "a \<up> 2 * b" then ()
 
   641 if UnparseC.term t = "a \<up> 2 * b" then ()
 
   642 else error "poly.sml: diff.behav. in make_polynomial 21";
 
   642 else error "poly.sml: diff.behav. in make_polynomial 21";
 
   643 
   643 
   644 "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
 
   644 "~~~~~ fun is_multUnordered , args:"; val (t) = (@{term "b * a * a::real"});
 
   645     ((is_polyexp t) andalso not (t = sort_variables t)) = true;  (*isa == isa2*)
 
   645     ((is_polyexp t) andalso not (t = sort_variables t)) = true;  (*isa == isa2*)
 
   658 
   658 
   659 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 
   659 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 
   660 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 
   660 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 
   661 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 
   661 "-------- fun is_multUnordered 2*3*a -----------------------------------------------------------";
 
   662 val t = TermC.str2term "2*3*a";
 
   662 val t = TermC.str2term "2*3*a";
 
   663 val SOME (t', _) = rewrite_set_ thy false make_polynomial t;
 
   663 val SOME (t', _) = rewrite_set_ ctxt false make_polynomial t;
 
   664 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
 
   664 (*+*)if UnparseC.term t' = "6 * a" then () else error "rewrite_set_ 2*3*a CHANGED";
 
   665 (*
 
   665 (*
 
   666 ##  try calc: "Groups.times_class.times" 
   666 ##  try calc: "Groups.times_class.times" 
   667 ##  rls: order_mult_rls_ on: 6 * a 
   667 ##  rls: order_mult_rls_ on: 6 * a 
   668 ###  rls: order_mult_ on: 6 * a 
   668 ###  rls: order_mult_ on: 6 * a 
   699 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
 
   699 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
 
   700 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
 
   700 "-------- norm_Poly with AlgEin ----------------------------------------------------------------";
 
   701 val thy = @{theory AlgEin};
 
   701 val thy = @{theory AlgEin};
 
   702 val ctxt = Proof_Context.init_global thy;
 
   702 val ctxt = Proof_Context.init_global thy;
 
   703 
   703 
   704 val SOME (f',_) = rewrite_set_ thy false norm_Poly
 
   704 val SOME (f',_) = rewrite_set_ ctxt false norm_Poly
 
   705 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
 
   705 (TermC.str2term "L = k - 2 * q + (k - 2 * q) + (k - 2 * q) + (k - 2 * q) + senkrecht + oben");
 
   706 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
 
   706 if UnparseC.term f' = "L = 2 * 2 * k + 2 * - 4 * q + senkrecht + oben"
 
   707 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
 
   707 then ((*norm_Poly NOT COMPLETE -- TODO MG*))
 
   708 else error "norm_Poly changed behavior";
 
   708 else error "norm_Poly changed behavior";
 
   709 (* isa:
 
   709 (* isa:
 
   728 
   728 
   729 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 
   729 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 
   730 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 
   730 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 
   731 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 
   731 "-------- complex examples from textbook Schalk I ----------------------------------------------";
 
   732 val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
 
   732 val t = TermC.str2term "1 + 2 * x \<up> 4 + 2 * - 2 * x \<up> 4 + x \<up> 8";
 
   733 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   733 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   734 if (UnparseC.term t) = "1 + - 2 * x \<up> 4 + x \<up> 8"
 
   734 if (UnparseC.term t) = "1 + - 2 * x \<up> 4 + x \<up> 8"
 
   735 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
 
   735 then () else error "poly.sml: diff.behav. in make_polynomial 9b";
 
   736 
   736 
   737 "-----SPB Schalk I p.64 No.296a ---";
 
   737 "-----SPB Schalk I p.64 No.296a ---";
 
   738 val t = TermC.str2term "(x - a) \<up> 3";
 
   738 val t = TermC.str2term "(x - a) \<up> 3";
 
   739 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   739 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   740 if (UnparseC.term t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
 
   740 if (UnparseC.term t) = "- 1 * a \<up> 3 + 3 * a \<up> 2 * x + - 3 * a * x \<up> 2 + x \<up> 3"
 
   741 then () else error "poly.sml: diff.behav. in make_polynomial 10";
 
   741 then () else error "poly.sml: diff.behav. in make_polynomial 10";
 
   742 
   742 
   743 "-----SPB Schalk I p.64 No.296c ---";
 
   743 "-----SPB Schalk I p.64 No.296c ---";
 
   744 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
 
   744 val t = TermC.str2term "(-3*x - 4*y) \<up> 3";
 
   745 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   745 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   746 if (UnparseC.term t) = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
 
   746 if (UnparseC.term t) = "- 27 * x \<up> 3 + - 108 * x \<up> 2 * y + - 144 * x * y \<up> 2 +\n- 64 * y \<up> 3"
 
   747 then () else error "poly.sml: diff.behav. in make_polynomial 11";
 
   747 then () else error "poly.sml: diff.behav. in make_polynomial 11";
 
   748 
   748 
   749 "-----SPB Schalk I p.62 No.242c ---";
 
   749 "-----SPB Schalk I p.62 No.242c ---";
 
   750 val t = TermC.str2term "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
 
   750 val t = TermC.str2term "x \<up> (- 4)*(x \<up> (- 4)*y \<up> (- 2)) \<up> (- 1)*y \<up> (- 2)";
 
   751 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   751 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   752 if (UnparseC.term t) = "1"
 
   752 if (UnparseC.term t) = "1"
 
   753 then () else error "poly.sml: diff.behav. in make_polynomial 12";
 
   753 then () else error "poly.sml: diff.behav. in make_polynomial 12";
 
   754 
   754 
   755 "-----SPB Schalk I p.60 No.209a ---";
 
   755 "-----SPB Schalk I p.60 No.209a ---";
 
   756 val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
 
   756 val t = TermC.str2term "a \<up> (7-x) * a \<up> x";
 
   757 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   757 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   758 if UnparseC.term t = "a \<up> 7"
 
   758 if UnparseC.term t = "a \<up> 7"
 
   759 then () else error "poly.sml: diff.behav. in make_polynomial 13";
 
   759 then () else error "poly.sml: diff.behav. in make_polynomial 13";
 
   760 
   760 
   761 "-----SPB Schalk I p.60 No.209d ---";
 
   761 "-----SPB Schalk I p.60 No.209d ---";
 
   762 val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
 
   762 val t = TermC.str2term "d \<up> x * d \<up> (x+1) * d \<up> (2 - 2*x)";
 
   763 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   763 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   764 if UnparseC.term t = "d \<up> 3"
 
   764 if UnparseC.term t = "d \<up> 3"
 
   765 then () else error "poly.sml: diff.behav. in make_polynomial 14";
 
   765 then () else error "poly.sml: diff.behav. in make_polynomial 14";
 
   766 
   766 
   767 
   767 
   768 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 
   768 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 
   769 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 
   769 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 
   770 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 
   770 "-------- complex Eigene Beispiele (Mathias Goldgruber) ----------------------------------------";
 
   771 "-----SPO ---";
 
   771 "-----SPO ---";
 
   772 val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
 
   772 val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
 
   773 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   773 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   774 if UnparseC.term t = "1" then ()
 
   774 if UnparseC.term t = "1" then ()
 
   775 else error "poly.sml: diff.behav. in make_polynomial 15";
 
   775 else error "poly.sml: diff.behav. in make_polynomial 15";
 
   776 
   776 
   777 "-----SPO ---";
 
   777 "-----SPO ---";
 
   778 val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
 
   778 val t = TermC.str2term "a \<up> 2*b*b \<up> (- 1)";
 
   779 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   779 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   780 if UnparseC.term t = "a \<up> 2" then ()
 
   780 if UnparseC.term t = "a \<up> 2" then ()
 
   781 else error "poly.sml: diff.behav. in make_polynomial 18";
 
   781 else error "poly.sml: diff.behav. in make_polynomial 18";
 
   782 "-----SPO ---";
 
   782 "-----SPO ---";
 
   783 val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
 
   783 val t = TermC.str2term "a \<up> 2*a \<up> (- 2)";
 
   784 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   784 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   785 if (UnparseC.term t) = "1" then ()
 
   785 if (UnparseC.term t) = "1" then ()
 
   786 else error "poly.sml: diff.behav. in make_polynomial 19";
 
   786 else error "poly.sml: diff.behav. in make_polynomial 19";
 
   787 "-----SPO ---";
 
   787 "-----SPO ---";
 
   788 val t = TermC.str2term "b + a - b";
 
   788 val t = TermC.str2term "b + a - b";
 
   789 val SOME (t,_) = rewrite_set_ thy false make_polynomial t; UnparseC.term t;
 
   789 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   790 if (UnparseC.term t) = "a" then ()
 
   790 if (UnparseC.term t) = "a" then ()
 
   791 else error "poly.sml: diff.behav. in make_polynomial 20";
 
   791 else error "poly.sml: diff.behav. in make_polynomial 20";
 
   792 
   792 
   793 "-----SPO ---";
 
   793 "-----SPO ---";
 
   794 val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
 
   794 val t = TermC.parseNEW' ctxt "a \<up> 2 * (-a) \<up> 2";
 
   795 val SOME (t,_) = rewrite_set_ @{theory} false make_polynomial t; UnparseC.term t;
 
   795 val SOME (t,_) = rewrite_set_ ctxt false make_polynomial t; UnparseC.term t;
 
   796 if (UnparseC.term t) = "a \<up> 4" then ()
 
   796 if (UnparseC.term t) = "a \<up> 4" then ()
 
   797 else error "poly.sml: diff.behav. in make_polynomial 24";
 
   797 else error "poly.sml: diff.behav. in make_polynomial 24";
wneuper/isa