"Testable"…"beta" version of Release 20071101 available now.
…I just uploaded another mmj2jar.zip and .md5 to
http://us2.metamath.org:8888/ocat/mmj2/mmj2jar.zip
and
http://us2.metamath.org:8888/ocat/mmj2/mmj2jar.md5
This version contains the following new feature (see the CHGLOG.TXT file in the mmj2jar.zip download for complete list):
(from CHGLOG.TXT):
6. Generates "info" message
"I-PA-0119 Theorem xyz RPN-format Metamath proof generated!"
when Ctrl-U (unification) is successful and the RPN-format
proof is generated. Previously, no message was output. Also,
positions to the last remaining (if any) incomplete proof
step -- or the 'qed' step if there are no incomplete proof
steps and the cursor has not already been set.
This modification allows a user to use a "dummy" 'qed'
step and incrementally build a proof, with cursor
positioning somewhere reasonable (a "dummy" incomplete
proof step could be manually input for this purpose.)
The new info message is intended to provide confirmation
of the success of unification -- which was previously
provided by positioning the cursor at the end of the
generated RPN-format proof.
—