test/Tools/isac/Knowledge/partial_fractions.sml
branchdecompose-isar
changeset 42315 c2e6ac4a5d04
parent 42313 f6a46e84067a
child 42352 52ffa99930b2
     1.1 --- a/test/Tools/isac/Knowledge/partial_fractions.sml	Thu Oct 13 13:46:30 2011 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/partial_fractions.sml	Thu Oct 13 15:03:28 2011 +0200
     1.3 @@ -27,10 +27,8 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem";
     1.5  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method";
     1.6  val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method";
     1.7 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
     1.8 -  "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
     1.9 -val (p,_,f,nxt,_,pt) = me nxt p [] pt; 
    1.10 -  "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
    1.11 +val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Rewrite (ruleZY, Inverse_Z_Transform.ruleZY) --> X z = 3 / (z - 1 / 4 + -1 / 8 * (1 / z))";
    1.12 +val (p''',_,f,nxt''',_,pt''') = me nxt p [] pt; "nxt = Rewrite_Set norm_Rational --> X' z = 3 / (z * (z - 1 / 4 + -1 / 8 * (1 / z)))";
    1.13  "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt);
    1.14  val ("ok", (_, _, ptp)) = locatetac tac (pt,p)
    1.15  val (pt, p) = ptp;