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

Thanks,
Rob

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

(defstep pp ()
    (postpone)
"" "" 
)