if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"

 if terms2str asms = "[\"a + b is_expanded\",\"c is_expanded\"]"

 then () else error "rewrite.sml: prepat cancel subst";

 then () else error "rewrite.sml: prepat cancel subst";

 if ([], true) = eval__true thy 0 asms [] erls

 if ([], true) = eval__true thy 0 asms [] erls

 then () else error "rewrite.sml: prepat cancel eval__true";

 then () else error "rewrite.sml: prepat cancel eval__true";

 (* if each pat* matches with the current term, the Rrls is applied

 (* if each pat* matches with the current term, the Rrls is applied

    (there are no preconditions to be checked, they are @{term True}) *)

    (there are no preconditions to be checked, they are @{term True}) *)

 val t = str2term "a / b + 1 / 2";

 val t = str2term "a / b + 1 / 2";

 val pat = parse_patt thy "?r / ?s + ?u / ?v";

 val pat = parse_patt thy "?r / ?s + ?u / ?v";

 val pres = [@{term True}];

 val pres = [@{term True}];

 val erls = rational_erls;

 val erls = rational_erls;

 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)

 (* erls got from Rrls {erls, prepat, scr = Rfuns {normal_form, ...}, ...} *)

 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);

 val subst = Pattern.match thy (pat, t) (Vartab.empty, Vartab.empty);

 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls

 if ([], true) = eval__true thy 0 (map (Envir.subst_term subst) pres) [] erls

 "===== Poly.thy: order_mult_ ===";

 "===== Poly.thy: order_mult_ ===";

           (* ?p matched with the current term gives an environment,

           (* ?p matched with the current term gives an environment,

              which evaluates (the instantiated) "p is_multUnordered" to true*)

              which evaluates (the instantiated) "p is_multUnordered" to true*)

 val t = str2term "x^^^2 * x";

 val t = str2term "x^^^2 * x";