test/Tools/isac/MathEngBasic/rewrite.sml
changeset 60405 d4ebe139100d
parent 60340 0ee698b0a703
child 60424 c3acf9c442ac
     1.1 --- a/test/Tools/isac/MathEngBasic/rewrite.sml	Thu Sep 16 12:23:57 2021 +0200
     1.2 +++ b/test/Tools/isac/MathEngBasic/rewrite.sml	Thu Sep 16 17:23:54 2021 +0200
     1.3 @@ -381,7 +381,7 @@
     1.4  (*+*)       (Const (\<^const_name>\<open>HOL.eq\<close>, _) $
     1.5  (*+*)         (Const (\<^const_name>\<open>is_multUnordered\<close>, _) $
     1.6  (*+*)           (Const (\<^const_name>\<open>times\<close>, _) $
     1.7 -(*+*)             (Const (\<^const_name>\<open>powr\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
     1.8 +(*+*)             (Const (\<^const_name>\<open>realpow\<close>, _) $ Free ("x", _) $ _ ) $ Free ("x", _))) $
     1.9  (*+*)         Const (\<^const_name>\<open>True\<close>, _))) => ()
    1.10  (*+*)(*                   ^^^^^^             compare ---vvv *)
    1.11  (*+*)| _ => error "rewrite.sml diff. eval_is_multUnordered 2b CHANGED";
    1.12 @@ -622,7 +622,7 @@
    1.13  (*+*)    Thm ("not_true", "(\<not> True) = False"),
    1.14  (*+*)    Thm ("not_false", "(\<not> False) = True"),
    1.15  (*+*)    :
    1.16 -(*+*)    Eval (\<^const_name>\<open>powr\<close>, fn),
    1.17 +(*+*)    Eval (\<^const_name>\<open>realpow\<close>, fn),
    1.18  (*+*)    Eval ("RatEq.is_ratequation_in", fn)]:
    1.19  (*+*)   rule list*)
    1.20  (*+*)chk: term list -> term list -> term list * bool