Mizar remote services updated

Dear Mizar users,

the Mizar remote verification/solving/presentation service at
http://mws.cs.ru.nl/~mptp/MizAR.html has now been updated to
include the latest MML version 4.160.1126, and installed also on
a new (faster) server at the University of Alberta:
http://mizar.cs.ualberta.ca/~mptp/MizAR.html . The version update
mechanism has been almost completely scripted, so new versions of
the service should be available automatically with new MML
versions.

An updated Mizar mode for Emacs is available at
https://github.com/JUrban/mizarmode/raw/master/mizar.el . This
now allows to customize the remote server, and switch on the use
of "by;" to trigger asynchronous ATP solving (see
http://mws.cs.ru.nl/~urban/ams11/out4.ogv for a demo).

Note that the ATP proofs now by default display also "implicit"
parts of Mizar reasoning, for example registrations. They are
written in the MMLQuery syntax, like : AFINSQ_1:exreg 2 (condreg
2, funcreg 2). If you need to look them up, just go to the
corresponding URL on mizar.org, e.g,
http://mizar.org/version/current/html/afinsq_1.html#RC2 (CC2,
FC2).

Best regards,
Josef Urban