1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Tue Jun 01 15:41:23 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Sat Jul 03 16:21:07 2021 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(* Title: "ProgLang/rewrite.sml"
     1.5 +(* Title: "MathEngBasic/rewrite.sml"
     1.6     Author: Walther Neuper 050908
     1.7     (c) copyright due to lincense terms.
     1.8  *)
     1.9 @@ -328,6 +328,7 @@
    1.10  val asms = map (Envir.subst_term subst) pres;
    1.11  if UnparseC.terms asms = "[\"a + b is_expanded\", \"c is_expanded\"]"
    1.12  then () else error "rewrite.sml: prepat cancel subst";
    1.13 +
    1.14  if ([], true) = eval__true thy 0 asms [] erls
    1.15  then () else error "rewrite.sml: prepat cancel eval__true";
    1.16  
    1.17 @@ -360,6 +361,7 @@
    1.18  val asms = map (Envir.subst_term subst) pres;
    1.19  if UnparseC.terms asms = "[\"x \<up> 2 * x is_multUnordered\"]"
    1.20  then () else error "rewrite.sml: prepat order_mult_ subst";
    1.21 +
    1.22  if ([], true) = eval__true thy 0 asms [] erls
    1.23  then () else error "rewrite.sml: prepat order_mult_ eval__true";
    1.24  
    1.25 @@ -371,7 +373,21 @@
    1.26  
    1.27  if is_multUnordered t then () else error "rewrite.sml diff. is_multUnordered 2";
    1.28  val tm = TermC.str2term "(x \<up> 2 * x) is_multUnordered";
    1.29 -eval_is_multUnordered "testid" "" tm thy;
    1.30 +
    1.31 +(*+*)case eval_is_multUnordered "testid" "" tm thy of
    1.32 +(*+*)  SOME
    1.33 +(*+*)    ("testidx \<up> 2 * x_",
    1.34 +(*+*)     Const ("HOL.Trueprop", _) $
    1.35 +(*+*)       (Const ("HOL.eq", _) $
    1.36 +(*+*)         (Const ("Poly.is_multUnordered", _) $
    1.37 +(*+*)           (Const ("Groups.times_class.times", _) $
    1.38 +(*+*)             (Const ("Transcendental.powr", _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
    1.39 +(*+*)         Const ("HOL.True", _))) => ()
    1.40 +(*+*)(*                   ^^^^^^             compare ---vvv *)
    1.41 +(*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
    1.42 +
    1.43 +
    1.44 +     eval_is_multUnordered "testid" "" tm thy;
    1.45  
    1.46  case eval_is_multUnordered "testid" "" tm thy of
    1.47      SOME (_, Const ("HOL.Trueprop", _) $ 
    1.48 @@ -613,7 +629,7 @@
    1.49  
    1.50             rewrite__set_ thy (i + 1) false bdv rls a (*of*);
    1.51  
    1.52 -(*+*)Rewrite.trace_on := true;
    1.53 +(*+*)Rewrite.trace_on := false;
    1.54  
    1.55          (*this was False; vvvv--- means: indeterminate*)
    1.56      val (* SOME (t, a') *)NONE = (*case*)
    1.57 @@ -671,7 +687,7 @@
    1.58  exception TERM raised (line 271 of "~~/src/HOL/Tools/hologic.ML"):
    1.59    dest_eq
    1.60    0 \<le> ?a \<Longrightarrow> (0 \<le> sqrt ?a) = True( **)
    1.61 -if UnparseC.term t = "x + 1 + -1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
    1.62 +if UnparseC.term t = "x + 1 + - 1 * 2 = 0" then () else error "rewrite_set_ norm_equation CHANGED";
    1.63  
    1.64  "~~~~~ fun rewrite_set_ , args:"; val (thy, bool, rls, term) = (thy, false, rls, term);
    1.65  "~~~~~ and rewrite__set_ , args:"; val (thy, i, put_asm, bdv, rls, ct) =