> In Pluscal, labels are attached to (sequences of) statements: they identify units of atomic execution. The fact that they
> can also serve as targets of goto statements is rather secondary. Typically, code snippets like the one that you show will > appear in a procedure, and you can use a return statement to terminate a procedure prematurely.
Sure but I don't like using PluCal procedure because you need to manage the stack in your proof then and it is
boring. I have just come across the Skip _expression_. I will try if we can use it for the discussed purpose.
--
FL