1.1 --- a/src/Tools/isac/Knowledge/Integrate.thy Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Integrate.thy Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -158,12 +158,12 @@
1.4 (*.for simplify_Integral adapted from 'norm_Rational_rls'.*)
1.5 val norm_Rational_rls_noadd_fractions =
1.6 Rule_Def.Repeat {id = "norm_Rational_rls_noadd_fractions", preconds = [],
1.7 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.8 + rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.9 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.10 rules = [(*Rule.Rls_ add_fractions_p_rls,!!!*)
1.11 Rule.Rls_ (*rat_mult_div_pow original corrected WN051028*)
1.12 (Rule_Def.Repeat {id = "rat_mult_div_pow", preconds = [],
1.13 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.14 + rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.15 erls = Rule_Set.append_rules "Rule_Set.empty-is_polyexp" Rule_Set.empty
1.16 [\<^rule_eval>\<open>is_polyexp\<close> (eval_is_polyexp "")],
1.17 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.18 @@ -187,7 +187,7 @@
1.19 (*.for simplify_Integral adapted from 'norm_Rational'.*)
1.20 val norm_Rational_noadd_fractions =
1.21 Rule_Set.Sequence {id = "norm_Rational_noadd_fractions", preconds = [],
1.22 - rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.23 + rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.24 erls = norm_rat_erls, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.25 rules = [Rule.Rls_ discard_minus,
1.26 Rule.Rls_ rat_mult_poly,(* removes double fractions like a/b/c *)
1.27 @@ -214,7 +214,7 @@
1.28 ];
1.29 val simplify_Integral =
1.30 Rule_Set.Sequence {id = "simplify_Integral", preconds = []:term list,
1.31 - rew_ord = ("dummy_ord", Rewrite_Ord.dummy_ord),
1.32 + rew_ord = ("dummy_ord", Rewrite_Ord.function_empty),
1.33 erls = Atools_erls, srls = Rule_Set.Empty,
1.34 calc = [], errpatts = [],
1.35 rules = [