[tlaplus] Discarded prototype TLA+ syntax: using @ inside proofs?

This is probably just another episode of me stumbling across and exhuming some long-discarded prototype syntax, but I wanted to make sure:

There are several places in the tools where there is a reference to use of the @ symbol in a proof context. We are all familiar with @ as used in [f EXCEPT ![n] = @ + 1], for example. Another place where you can use @, not as familiar, is in subexpressions like op!<<!@. If you don't know what subexpressions are then worry not, Lamport views them as a mistake and hopes they get removed from the language. My understanding of the meaning of @ in subexpressions is that they let you turn an unbound quantifier like op == \A x : f[x] into the operator op(x) == f[x] by going op!@. Turn unbound quantifiers into LAMBDAs, basically. But anyway, back on topic - is there yet another (deprecated?) use of @ in the language?

The first place I noticed this was in the TLAPM parser; the "At" _expression_ variant takes a boolean parameter, with the curious comment:

`true` means `@` from `EXCEPT`, and
`false` means `@` from a proof step.

I didn't understand what this was about, thinking perhaps EXCEPT statements require special handling when used inside proofs. As far as I can tell the only attempt to construct an "At true" variant in the TLAPM parser is commented out, so the boolean parameter might just be some zombie thing.

Then I was looking at how subexpressions are implemented in SANY, and found this curious comment:

An assertion or ASSUME/PROVE step is represented as an
ordinary theorem, so the object's getTheorem() node
returns the ExprNode or AssumeProveNode that is the
assertion made by the step. The object's isSuffices()
method returns false.

As a special case, a step of the form "@ infixop _expression_"
has as its theorem an OpApplNode whose first argument is an
OpApplNode with operator $Nop and argument (a reference to)
the right-hand-side _expression_ of the previous step.

So here's another hint about something involving @ and proofs, this time having to do with the rather complicated ASSUME/PROVE construct. ASSUME/PROVE blocks can include nested ASSUME/PROVEs which can be labelled, and labels are types of subexpressions, so @ having some meaning in the context of ASSUME/PROVE blocks is not unthinkable (also, "$Nop" is what SANY uses as the subexpression opcode, don't ask why).

Does anybody know more about this topic? Is this some deprecated syntax like temporal ASSUME/PROVE or does it still exist in some form in the language?

Thanks!

Andrew Helwer