| author | Walther Neuper <neuper@ist.tugraz.at> |
| Fri, 23 Sep 2011 16:22:11 +0200 | |
| branch | decompose-isar |
| changeset 42289 | 801b5f1154bf |
| child 42301 | 93083d4e05d8 |
| permissions | -rw-r--r-- |
| neuper@42289 | 1 |
(* Title: partial fraction decomposition |
| neuper@42289 | 2 |
Author: Jan Rocnik |
| neuper@42289 | 3 |
(c) due to copyright terms |
| neuper@42289 | 4 |
*) |
| neuper@42289 | 5 |
|
| neuper@42289 | 6 |
"--------------------------------------------------------"; |
| neuper@42289 | 7 |
"table of contents --------------------------------------"; |
| neuper@42289 | 8 |
"--------------------------------------------------------"; |
| neuper@42289 | 9 |
"----------- get_denominator ----------------------------"; |
| neuper@42289 | 10 |
"--------------------------------------------------------"; |
| neuper@42289 | 11 |
"--------------------------------------------------------"; |
| neuper@42289 | 12 |
"--------------------------------------------------------"; |
| neuper@42289 | 13 |
|
| neuper@42289 | 14 |
|
| neuper@42289 | 15 |
"----------- get_denominator ----------------------------"; |
| neuper@42289 | 16 |
"----------- get_denominator ----------------------------"; |
| neuper@42289 | 17 |
"----------- get_denominator ----------------------------"; |
| neuper@42289 | 18 |
val t = @{term "a/(b::real)"};
|
| neuper@42289 | 19 |
val SOME (str, t') = eval_get_denominator "" 0 t @{theory Isac};
|
| neuper@42289 | 20 |
if term2str t' = "a / b = b" then () else error "eval_get_denominator"; |
| neuper@42289 | 21 |
|
| neuper@42289 | 22 |