104 TODOs for this version are in partial_fractions.sml "--- progr.vers.2: " |
104 TODOs for this version are in partial_fractions.sml "--- progr.vers.2: " |
105 \<close> |
105 \<close> |
106 |
106 |
107 ML \<open> |
107 ML \<open> |
108 val ansatz_rls = prep_rls'( |
108 val ansatz_rls = prep_rls'( |
109 Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
109 Rule_Def.Repeat {id = "ansatz_rls", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
110 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
110 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
111 rules = [ |
111 rules = [ |
112 \<^rule_thm>\<open>ansatz_2nd_order\<close>, |
112 \<^rule_thm>\<open>ansatz_2nd_order\<close>, |
113 \<^rule_thm>\<open>ansatz_3rd_order\<close>], |
113 \<^rule_thm>\<open>ansatz_3rd_order\<close>], |
114 scr = Rule.Empty_Prog}); |
114 scr = Rule.Empty_Prog}); |
115 |
115 |
116 val equival_trans = prep_rls'( |
116 val equival_trans = prep_rls'( |
117 Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
117 Rule_Def.Repeat {id = "equival_trans", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
118 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
118 erls = Rule_Set.Empty, srls = Rule_Set.Empty, calc = [], errpatts = [], |
119 rules = [ |
119 rules = [ |
120 \<^rule_thm>\<open>equival_trans_2nd_order\<close>, |
120 \<^rule_thm>\<open>equival_trans_2nd_order\<close>, |
121 \<^rule_thm>\<open>equival_trans_3rd_order\<close>], |
121 \<^rule_thm>\<open>equival_trans_3rd_order\<close>], |
122 scr = Rule.Empty_Prog}); |
122 scr = Rule.Empty_Prog}); |
123 |
123 |
124 val multiply_ansatz = prep_rls'( |
124 val multiply_ansatz = prep_rls'( |
125 Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.dummy_ord), |
125 Rule_Def.Repeat {id = "multiply_ansatz", preconds = [], rew_ord = ("dummy_ord",Rewrite_Ord.function_empty), |
126 erls = Rule_Set.Empty, |
126 erls = Rule_Set.Empty, |
127 srls = Rule_Set.Empty, calc = [], errpatts = [], |
127 srls = Rule_Set.Empty, calc = [], errpatts = [], |
128 rules = [ |
128 rules = [ |
129 \<^rule_thm>\<open>multiply_2nd_order\<close>], |
129 \<^rule_thm>\<open>multiply_2nd_order\<close>], |
130 scr = Rule.Empty_Prog}); |
130 scr = Rule.Empty_Prog}); |