I'd like some way of skipping forward 'n' goals in a proof, ie a
generalisation of the postpone rule. I've tried defining my own but
with no luck (I can't even get an abbreviation of postpone to work).
Is there a way of doing this (from the Rule? prompt)?
Thanks,
Rob
For me, the following strategy has no effect when applied.
(defstep pp ()
(postpone)
"" ""
)