1.1 --- a/src/Tools/isac/Knowledge/Partial_Fractions.thy Wed Aug 03 18:17:27 2022 +0200
1.2 +++ b/src/Tools/isac/Knowledge/Partial_Fractions.thy Thu Aug 04 12:48:37 2022 +0200
1.3 @@ -106,7 +106,7 @@
1.4
1.5 ML \<open>
1.6 val ansatz_rls = prep_rls'(
1.7 - Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.8 + Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.9 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.10 rules = [
1.11 \<^rule_thm>\<open>ansatz_2nd_order\<close>,
1.12 @@ -114,7 +114,7 @@
1.13 scr = Rule.Empty_Prog});
1.14
1.15 val equival_trans = prep_rls'(
1.16 - Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.17 + Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.18 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [],
1.19 rules = [
1.20 \<^rule_thm>\<open>equival_trans_2nd_order\<close>,
1.21 @@ -122,7 +122,7 @@
1.22 scr = Rule.Empty_Prog});
1.23
1.24 val multiply_ansatz = prep_rls'(
1.25 - Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord),
1.26 + Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty),
1.27 erls = Rule_Set.Empty,
1.28 srls = Rule_Set.Empty, calc = [], errpatts = [],
1.29 rules = [