checked tests for cancel_p start_Take
authorwneuper
Tue, 05 Sep 2006 17:06:37 +0200
branchstart_Take
changeset 653f2ef81c19028
parent 652 8d7ffa38b637
child 654 7bfcb1e870ed
checked tests for cancel_p
src/smltest/IsacKnowledge/rational.sml
     1.1 --- a/src/smltest/IsacKnowledge/rational.sml	Tue Sep 05 16:54:36 2006 +0200
     1.2 +++ b/src/smltest/IsacKnowledge/rational.sml	Tue Sep 05 17:06:37 2006 +0200
     1.3 @@ -1368,21 +1368,18 @@
     1.4  (*Schalk I, p.68 Nr. 437b *)
     1.5  (* SK loops, Falsches Ergebnis: cancel_p kann nicht weiter krzen!!! *)
     1.6  val t = str2term "(a + b)/(x^^^2 - y^^^2) * ((x - y)^^^2/(a^^^2 - b^^^2))";
     1.7 +(*
     1.8  val Some (t,_) = rewrite_set_ thy false norm_Rational(*_mg*) t;
     1.9  term2str t; WN060831????SK9
    1.10  "(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)";
    1.11 -
    1.12 -(**)
    1.13 +*)
    1.14  
    1.15  (* *)
    1.16  val t = str2term 
    1.17  "(a * x ^^^ 2 + -2 * a * x * y + a * y ^^^ 2 + b * x ^^^ 2 + -2 * b * x * y + b * y ^^^ 2) /(a ^^^ 2 * x ^^^ 2 + -1 * a ^^^ 2 * y ^^^ 2 + -1 * b ^^^ 2 * x ^^^ 2 + b ^^^ 2 * y ^^^ 2)"; 
    1.18 -(* WN060831????SK10 *)
    1.19 +(* WN060831????SK10 
    1.20  val Some (t,_) = rewrite_set_ thy false cancel_p t;
    1.21  term2str t;
    1.22 -(*
    1.23 -uncaught exception nonexhaustive binding failure
    1.24 -  raised at: stdIn:270.1-270.51
    1.25  *)
    1.26  
    1.27  (*SRM Schalk I, p.68 Nr. 438a *)