1.1 --- a/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 14:08:09 2006 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Mon Sep 04 14:10:45 2006 +0200
     1.3 @@ -410,6 +410,7 @@
     1.4  (*sometime before 060831???SK3..*)"((-1) - y - x) / (y - x)";
     1.5  (*WN.16.10.02             lexicographische Ordnung  ^^^^^^^ ?!*)
     1.6  
     1.7 +
     1.8    val t=(term_of o the o (parse thy)) 
     1.9    	    "(y^^^2 - x^^^2)/(y^^^2 - 2*y*x + x^^^2)";
    1.10    val Some (t',_) = norm_expanded_rat_ thy t;
    1.11 @@ -498,7 +499,7 @@
    1.12  val e188c'="( a + -1 * b ) / ( b + -1 * a )";
    1.13  val e188c = the (rewrite_set thy' false "cancel" e188c');
    1.14    is_expanded (parse_rat "a + -1 * b");
    1.15 -  false; -----------!!! WN060831???SK5*)
    1.16 +  false; -----------!!! WN060831???SK5 geht am worksheet?!?*)
    1.17  val Some (t,_) = 
    1.18      rewrite_set thy' false mp "((-1)*(b + (-1) * a))/(1*(b + (-1) * a))";
    1.19  if t= "(a + -1 * b) / (-1 * a + b)"  then()
    1.20 @@ -2088,4 +2089,17 @@
    1.21  
    1.22  val t = str2term "a*(b*(c*d)) / (b*(e*(f*g)))";
    1.23  val Some (t', _) = cancel_p_ thy t; term2str t';
    1.24 -(*???SK order ???*)
    1.25 \ No newline at end of file
    1.26 +(*???SK order ???*)
    1.27 +
    1.28 +val t = str2term "(x^^^2 - y^^^2)/(x^^^2 - 2*x*y + y^^^2) + 1 / (x - y)";
    1.29 +val Some (t',_) = common_nominator_ thy t;
    1.30 +val Some (t'',_) = add_fraction_ thy t;
    1.31 +term2str t' =
    1.32 +"(-1 * y ^^^ 2 + x ^^^ 2) / ((-1 * y + x) * (-1 * y + x)) +\n1\
    1.33 +\ * (-1 * y + x) / ((-1 * y + x) * (-1 * y + x))" (*true*);
    1.34 +term2str t'' = "(-1 - y - x) / (1 * y - x)" (*true*);
    1.35 +(*sometime before 060831???SK3..*)
    1.36 +"((-1) * y ^^^ 2 + x ^^^ 2) / (((-1) * y + x) * ((-1) * y + x)) +\
    1.37 +\1 * ((-1) * y + x) / (((-1) * y + x) * ((-1) * y + x))";
    1.38 +(*sometime before 060831???SK3..*)"((-1) - y - x) / (y - x)";
    1.39 +(*WN.16.10.02             lexicographische Ordnung  ^^^^^^^ ?!*)