TLAPM parser does not accept INSTANCE proof step type

[ahelwer]

Quoting from TLA Version 2: A Preliminary Guide [pdf], section 7.5.2 on page 27:

An INSTANCE step consists of a step-starting token followed by an ordinary INSTANCE statement (one that begins with the keyword INSTANCE). It has the same effect on the state as the corresponding (top-level) statement.

So I guess this is a way of introducing a module instance to get its definitions in scope in the middle of a proof. Anyway, TLAPM's syntax parser does not accept this; SANY does:

---- MODULE Test ----
THEOREM TRUE
<1>a. INSTANCE M
<1>b. QED
====

Ref #159