equal
deleted
inserted
replaced
270 |
270 |
271 "----------- progr.vers.2: check erls for multiply_ansatz"; |
271 "----------- progr.vers.2: check erls for multiply_ansatz"; |
272 "----------- progr.vers.2: check erls for multiply_ansatz"; |
272 "----------- progr.vers.2: check erls for multiply_ansatz"; |
273 "----------- progr.vers.2: check erls for multiply_ansatz"; |
273 "----------- progr.vers.2: check erls for multiply_ansatz"; |
274 (*test for outcommented 3 lines in script: is norm_Rational strong enough?*) |
274 (*test for outcommented 3 lines in script: is norm_Rational strong enough?*) |
275 val t = TermC.str2term "(3 / ((- 1 + - 2 * z + 8 * z \<up> 2) *3/24)) = (3 / ((z - 1 / 2) * (z - - 1 / 4)))"; |
275 val t = TermC.parse_test @{context} "(3 / ((- 1 + - 2 * z + 8 * z \<up> 2) *3/24)) = (3 / ((z - 1 / 2) * (z - - 1 / 4)))"; |
276 val SOME (t', _) = rewrite_set_ @{theory Isac_Knowledge} true ansatz_rls t; |
276 val SOME (t', _) = rewrite_set_ @{theory Isac_Knowledge} true ansatz_rls t; |
277 UnparseC.term t' = "3 / ((- 1 + - 2 * z + 8 * z \<up> 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - - 1 / 4)"; |
277 UnparseC.term t' = "3 / ((- 1 + - 2 * z + 8 * z \<up> 2) * 3 / 24) =\n?A / (z - 1 / 2) + ?B / (z - - 1 / 4)"; |
278 |
278 |
279 val SOME (t'', _) = rewrite_set_ @{theory Isac_Knowledge} true multiply_ansatz t'; (*true*) |
279 val SOME (t'', _) = rewrite_set_ @{theory Isac_Knowledge} true multiply_ansatz t'; (*true*) |
280 UnparseC.term t'' = "(z - 1 / 2) * (z - - 1 / 4) * 3 / ((- 1 + - 2 * z + 8 * z \<up> 2) * 3 / 24) =\n" ^ |
280 UnparseC.term t'' = "(z - 1 / 2) * (z - - 1 / 4) * 3 / ((- 1 + - 2 * z + 8 * z \<up> 2) * 3 / 24) =\n" ^ |