1 (* Title: partial fraction decomposition
3 (c) due to copyright terms
6 "--------------------------------------------------------";
7 "table of contents --------------------------------------";
8 "--------------------------------------------------------";
9 "----------- get_denominator ----------------------------";
10 "--------------------------------------------------------";
11 "--------------------------------------------------------";
12 "--------------------------------------------------------";
15 "----------- get_denominator ----------------------------";
16 "----------- get_denominator ----------------------------";
17 "----------- get_denominator ----------------------------";
18 val t = @{term "a/(b::real)"};
19 val SOME (str, t') = eval_get_denominator "" 0 t @{theory Isac};
20 if term2str t' = "a / b = b" then () else error "eval_get_denominator";