test/Tools/isac/BaseDefinitions/rewrite-order.sml
changeset 60565 f92963a33fe3
parent 60500 59a3af532717
child 60586 007ef64dbb08
     1.1 --- a/test/Tools/isac/BaseDefinitions/rewrite-order.sml	Sun Oct 09 06:53:03 2022 +0200
     1.2 +++ b/test/Tools/isac/BaseDefinitions/rewrite-order.sml	Sun Oct 09 07:44:22 2022 +0200
     1.3 @@ -17,7 +17,7 @@
     1.4  "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";
     1.5  "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";
     1.6  "-------- identify difference in term-order between isa=NEW, isa2+OLD --------------------------";
     1.7 -val form = TermC.str2term "x + -2 ::real"
     1.8 +val form = TermC.parse_test @{context} "x + -2 ::real"
     1.9  val Repeat {rew_ord = ("sqrt_right", rew_ord_), erls, ...} = Test_simplify;
    1.10  val ctxt = Proof_Context.init_global @{theory Test};
    1.11  (*Rewrite.trace_on := false; (*true false*)*)