equal
deleted
inserted
replaced
153 (* ((a/b) / (c/d) = (a*d) / (b*c)) *) |
153 (* ((a/b) / (c/d) = (a*d) / (b*c)) *) |
154 Rule.Thm("rat_double_rat_3",ThmC.numerals_to_Free @{thm rat_double_rat_3}) |
154 Rule.Thm("rat_double_rat_3",ThmC.numerals_to_Free @{thm rat_double_rat_3}) |
155 (* ((a/b) / c = a / (b*c) ) *)], |
155 (* ((a/b) / c = a / (b*c) ) *)], |
156 scr = Rule.Empty_Prog}); |
156 scr = Rule.Empty_Prog}); |
157 \<close> |
157 \<close> |
158 setup_rule rateq_erls = rateq_erls |
158 rule_set_knowledge rateq_erls = rateq_erls |
159 setup_rule RatEq_eliminate = RatEq_eliminate |
159 rule_set_knowledge RatEq_eliminate = RatEq_eliminate |
160 setup_rule RatEq_simplify = RatEq_simplify |
160 rule_set_knowledge RatEq_simplify = RatEq_simplify |
161 |
161 |
162 subsection \<open>problems\<close> |
162 subsection \<open>problems\<close> |
163 setup \<open>KEStore_Elems.add_pbts |
163 setup \<open>KEStore_Elems.add_pbts |
164 [(Problem.prep_input thy "pbl_equ_univ_rat" [] Problem.id_empty |
164 [(Problem.prep_input thy "pbl_equ_univ_rat" [] Problem.id_empty |
165 (["rational", "univariate", "equation"], |
165 (["rational", "univariate", "equation"], |