test/Tools/isac/Interpret/mathengine.sml
branchdecompose-isar
changeset 41950 2476f5f0f9ee
parent 41949 c1859b72ae8d
parent 41943 f33f6959948b
child 41952 0e76e17a430a
equal deleted inserted replaced
41949:c1859b72ae8d 41950:2476f5f0f9ee
   130 
   130 
   131 "===== input a formula to be derived from previous istate";
   131 "===== input a formula to be derived from previous istate";
   132 "----- appendFormula TODO: first repair error";
   132 "----- appendFormula TODO: first repair error";
   133   val cs = ((pt,p),[]);
   133   val cs = ((pt,p),[]);
   134   val ("ok", cs' as (_,_,(pt,p))) = step p cs;
   134   val ("ok", cs' as (_,_,(pt,p))) = step p cs;
   135   val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2"; val encode = I;
   135   val ifo = (* encode "4^^^2" \<longrightarrow>*) "4^2";
   136 (*
   136 (*
   137   val ("no derivation found", (_,_,(pt, p))) = inform cs' (encode ifo);
   137   val ("no derivation found", (_,_,(pt, p))) = inform cs' ((*encode*) ifo);
   138   here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
   138   here ^^^^^^^^^^^^^^^^^^^^^ should be "ok"
   139 *)
   139 *)
   140 
   140 
   141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   141 val (p,_,f,nxt,_,pt) = me nxt p [1] pt;
   142 (*nxt = ("Calculate",Calculate "DIVIDE")*)
   142 (*nxt = ("Calculate",Calculate "DIVIDE")*)