test/Tools/isac/Knowledge/partial_fractions.sml
branchdecompose-isar
changeset 42289 801b5f1154bf
child 42301 93083d4e05d8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Fri Sep 23 16:22:11 2011 +0200
     1.3 @@ -0,0 +1,22 @@
     1.4 +(* Title:  partial fraction decomposition
     1.5 +   Author: Jan Rocnik
     1.6 +   (c) due to copyright terms
     1.7 +*)
     1.8 +
     1.9 +"--------------------------------------------------------";
    1.10 +"table of contents --------------------------------------";
    1.11 +"--------------------------------------------------------";
    1.12 +"----------- get_denominator ----------------------------";
    1.13 +"--------------------------------------------------------";
    1.14 +"--------------------------------------------------------";
    1.15 +"--------------------------------------------------------";
    1.16 +
    1.17 +
    1.18 +"----------- get_denominator ----------------------------";
    1.19 +"----------- get_denominator ----------------------------";
    1.20 +"----------- get_denominator ----------------------------";
    1.21 +val t = @{term "a/(b::real)"};
    1.22 +val SOME (str, t') = eval_get_denominator "" 0 t @{theory Isac};
    1.23 +if term2str t' = "a / b = b" then () else error "eval_get_denominator";
    1.24 +
    1.25 +