34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem"; |
34 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Problem"; |
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method"; |
35 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "Specify_Method"; |
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method"; |
36 val (p,_,f,nxt,_,pt) = me nxt p [] pt; "nxt = Apply_Method"; |
37 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))"; |
37 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))"; |
38 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)))"; |
38 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)))"; |
39 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ptree)) = (nxt, p, [], pt); |
39 "~~~~~ fun me, args:"; val ((_,tac), (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt); |
40 val ("ok", (_, _, ptp)) = locatetac tac (pt,p) |
40 val ("ok", (_, _, ptp)) = locatetac tac (pt,p) |
41 val (pt, p) = ptp; |
41 val (pt, p) = ptp; |
42 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
42 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
43 (p, ((pt, e_pos'),[])); |
43 (p, ((pt, e_pos'),[])); |
44 val pIopt = get_pblID (pt,ip); |
44 val pIopt = get_pblID (pt,ip); |
53 |
53 |
54 "----------- why not nxt = Model_Problem here ? ---------"; |
54 "----------- why not nxt = Model_Problem here ? ---------"; |
55 "----------- why not nxt = Model_Problem here ? ---------"; |
55 "----------- why not nxt = Model_Problem here ? ---------"; |
56 "----------- why not nxt = Model_Problem here ? ---------"; |
56 "----------- why not nxt = Model_Problem here ? ---------"; |
57 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; |
57 val (p,_,f,nxt,_,pt) = me nxt''' p''' [] pt'''; |
58 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ptree)) = (nxt, p, c, pt); |
58 "~~~~~ fun me, args:"; val (((_,tac):tac'_), (p:pos'), _, (pt:ctree)) = (nxt, p, c, pt); |
59 val ("ok", (_, _, ptp)) = locatetac tac (pt,p); |
59 val ("ok", (_, _, ptp)) = locatetac tac (pt,p); |
60 val (pt, p) = ptp; |
60 val (pt, p) = ptp; |
61 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
61 "~~~~~ fun step, args:"; val (((ip as (_,p_)):pos'), ((ptp as (pt,p), tacis):calcstate)) = |
62 (p, ((pt, e_pos'),[])); |
62 (p, ((pt, e_pos'),[])); |
63 val pIopt = get_pblID (pt,ip); |
63 val pIopt = get_pblID (pt,ip); |