test/Tools/isac/Knowledge/polyeq-1.sml
changeset 59920 33913fe24685
parent 59903 5037ca1b112b
child 59921 0766dade4a78
     1.1 --- a/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Apr 29 09:03:01 2020 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/polyeq-1.sml	Wed Apr 29 12:30:51 2020 +0200
     1.3 @@ -352,7 +352,7 @@
     1.4  val (p,_,f,nxt,_,pt) = me nxt p [] pt; (*nxt =..,Check_elementwise "Assumptions")*)
     1.5  "~~~~~ fun me, args:"; val (tac, (p:pos'), _, (pt:ctree)) = (nxt, p, [], pt);
     1.6  "~~~~~ fun Step.by_tactic, args:"; val (tac, (ptp as (pt, p))) = (tac, (pt, p));
     1.7 -val Appl m = applicable_in p pt tac;
     1.8 +val Applicable.Yes m = applicable_in p pt tac;
     1.9  val Check_elementwise' (trm1, str, (trm2, trms)) = m;
    1.10  UnparseC.term trm1 = "[z = 1 / 8 + sqrt (9 / 16) / 2, z = 1 / 8 + -1 * sqrt (9 / 16) / 2]";
    1.11  str = "Assumptions";