test/Tools/isac/Knowledge/polyminus.sml
changeset 60575 5b936d0aed05
parent 60571 19a172de0bb5
child 60586 007ef64dbb08
     1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml	Fri Oct 21 15:19:00 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml	Fri Oct 21 15:35:50 2022 +0200
     1.3 @@ -659,7 +659,7 @@
     1.4  "----------- Refine.refine Vereinfache ----------------------------------";
     1.5  val fmz = ["Term (8*(a - q) + a - 2*q + 3*(a - 2*(q::real)))", "normalform (N::real)"];
     1.6  (*default_print_depth 11;*)
     1.7 -val matches = Refine.refine_PIDE @{context} fmz ["vereinfachen"];
     1.8 +val matches = Refine.xxxxx @{context} fmz ["vereinfachen"];
     1.9  (*default_print_depth 3;*)
    1.10  
    1.11  "----- go into details, if it seems not to work -----";