240 val t = (term_of o the o (parse thy)) |
240 val t = (term_of o the o (parse thy)) |
241 "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)"; |
241 "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)"; |
242 val (t,asm) = the (rewrite_set_ thy eval_rls false rls t); |
242 val (t,asm) = the (rewrite_set_ thy eval_rls false rls t); |
243 |
243 |
244 |
244 |
245 val thy' = "Rational.thy"; |
245 val thy' = "Rational"; |
246 val rls' = "cancel"; |
246 val rls' = "cancel"; |
247 val t' = "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)"; |
247 val t' = "(1 + 1 * a ^^^ 1)///(-2 + 2 * a ^^^ 2)"; |
248 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); |
248 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); |
249 (*if t' = "1 /// (-2 + 2 * a)" then () |
249 (*if t' = "1 /// (-2 + 2 * a)" then () |
250 else raise error "tests/rationals.sml(1): new behaviour";*) |
250 else raise error "tests/rationals.sml(1): new behaviour";*) |
251 |
251 |
252 |
252 |
253 val thy' = "Rational.thy"; |
253 val thy' = "Rational"; |
254 val rls' = "cancel"; |
254 val rls' = "cancel"; |
255 val t' = "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// (5 * a * b * c + 7 * a^^^2 * b * c) "; |
255 val t' = "(10 * a^^^2 * b * c + 14 * a * b + 3 * a * c + 20 * a * b^^^2 * c) /// (5 * a * b * c + 7 * a^^^2 * b * c) "; |
256 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); |
256 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); |
257 |
257 |
258 val thy' = "Rational.thy"; |
258 val thy' = "Rational"; |
259 val rls' = "cancel"; |
259 val rls' = "cancel"; |
260 val t' = "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )"; |
260 val t' = "(a^^^2 * b + 2 * a * b + b ) /// ( a^^^2 - 1 )"; |
261 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); |
261 val (t',asm') = the (rewrite_set thy' "eval_rls" false rls' t'); |
262 |
262 |
263 (* |
263 (* |