1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Thu Oct 06 16:15:29 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Thu Oct 06 17:43:00 2011 +0200
     1.3 @@ -48,6 +48,7 @@
     1.4  "-------- investigate rulesets for cancel_p -------------";
     1.5  "-------- investigate format of factout_ and factout_p_ -";
     1.6  "-------- how to stepwise construct Scripts -------------";
     1.7 +"----------- get_denominator ----------------------------";
     1.8  "--------------------------------------------------------";
     1.9  "--------------------------------------------------------";
    1.10  "--------------------------------------------------------";
    1.11 @@ -2078,3 +2079,13 @@
    1.12  "    Try (Rewrite_Set discard_parentheses False))               " ^
    1.13  "   t_t)"
    1.14  );
    1.15 +
    1.16 +"----------- get_denominator ----------------------------";
    1.17 +"----------- get_denominator ----------------------------";
    1.18 +"----------- get_denominator ----------------------------";
    1.19 +val thy = @{theory Isac};
    1.20 +val t = term_of (the (parse thy "get_denominator ((a +x)/b)"));
    1.21 +val SOME (_, t') = eval_get_denominator "" 0 t thy;
    1.22 +if term2str t' = "get_denominator ((a + x) / b) = b" then ()
    1.23 +else error "get_denominator ((a + x) / b) = b"
    1.24 +