test/Tools/isac/Knowledge/rational.sml
changeset 52096 ee2a5f066e44
parent 52095 c9fbb8171a0a
child 52100 0831a4a6ec8a
     1.1 --- a/test/Tools/isac/Knowledge/rational.sml	Wed Aug 28 11:48:37 2013 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/rational.sml	Fri Aug 30 13:43:30 2013 +0200
     1.3 @@ -346,6 +346,11 @@
     1.4  "-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------";
     1.5  "-------- cancel_p from: Mathematik 1 Schalk Reniets Verlag ------------------";
     1.6  val thy  = @{theory "Rational"};
     1.7 +"-------- WN";
     1.8 +val t = str2term "(2 + -3 * x) / 9";
     1.9 +if NONE = rewrite_set_ thy false cancel_p t then ()
    1.10 +else error "rewrite_set_ cancel_p must return NONE, if the term cannot be cancelled";
    1.11 +
    1.12  "-------- example 186a";
    1.13  val t = str2term "(14 * x * y) / (x * y)";
    1.14    is_expanded (str2term "14 * x * y");