[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] postponing 'n' goals

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)?


For me, the following strategy has no effect when applied.

(defstep pp ()
"" ""