2016-05-13 9:49 GMT+02:00 Hendrik Tews <hendrik.t...@fireeye.com>:
> For 2 and 5 I insert additional print commands into the queue of
> commands. Because you cannot print wrt. an old state, these print
> commands need to be inserted directly after the command that
> generates additional subgoals or that instantiate existential
> variables.

This might change with the idesave + Stm protocol.

Paul are you using the Stm stuff?

ProofGeneral-devel mailing list

Reply via email to