ATP and presentation service for Mizar updated to MML 5.23.1213

Dear Mizar Users,

the ATP and presentation service for Mizar (MizAR) has now been
updated to the latest Mizar/MML version 5.23.1213.

As before, the recommended use is from Emacs. The main functions are:

- pressing ";" directly after the "by" keyword calls ATP systems on
the current proposition
- pressing C-c h any time opens a HTML-ized version of the article in a browser

The older video demonstrating the use is here:
http://mws.cs.ru.nl/~urban/ams11/out4.ogv

Common pitfalls:

- If "by;" does not work at all, check that you are using one of the
supported MML versions by looking at the available MML version values
at http://mizar.cs.ualberta.ca/~mptp/MizAR.html (MML versions 1213 and
1147 are running the strongest ATP and recommending systems).

- Check that the value of the Emacs variable mizar-atp-completion is
"t" (this should be the default).

- The value of the Emacs variable ar4mizar-server should be
"http://mizar.cs.ualberta.ca/" (Piotr is still helping your Mizaring
from afar)

- The normal response time should be between 10 - 30 seconds (each
proof attempt now learns from some 60k MML proofs in several ways and
considers some 150k formulas), depending on the size of your
environment. If your article takes more than several seconds to
verify, use the ::$P- and ::$P+ directives (formerly @proof) to switch
off proof-checking of unnecessary parts.

If things still don't work, let me know.

More details about the service are here:
http://dx.doi.org/10.1007/s10817-012-9269-y . Details of the latest
strengthening done with very fast machine-learning systems with Cezary
Kaliszyk is described here: http://arxiv.org/abs/1310.2805 .

Best,
Josef