1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml Tue Feb 11 10:59:18 2020 +0100
1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml Tue Feb 11 11:58:45 2020 +0100
1.3 @@ -183,7 +183,7 @@
1.4 (*[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2] TODO sqrt*)
1.5 val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
1.6 "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
1.7 -"~~~~~ fun locatetac, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.8 +"~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
1.9 val Appl m = applicable_in p pt tac;
1.10 val Check_elementwise' (trm1, str, (trm2, trms)) = m;
1.11 term2str trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";