[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] tooltips
Hi,
the HTML/ATP services now use tooltips (balloon help as in Emacs) for
showing thesis, the meaning of the used library references, the
meaning of property/correctness formulas, proofs, and ATP
explanations. Clicking should work as before (it seems good to combine
both these methods when reading proofs).
A normal example is
http://mizar.cs.ualberta.ca/~mptp/7.13.01_4.181.1147/html/card_1.html
. An example with tooltips over the "by/from" keywords showing also
ATP explanations is
http://mizar.cs.ualberta.ca/~mptp/cgi-bin/MizAR.cgi?ProblemSource=URL&FormulaURL=http://mizar.cs.ualberta.ca/~mptp/mml4.181.1147/mml/card_1.miz&MMLVersion=4.181.1147&Name=Tst1&GenATP=1&HTMLize=1
(or use the interface at http://mizar.cs.ualberta.ca/~mptp/MizAR.html,
or the html-ization from Emacs).
I have only tested with Firefox and Chrome so far, no idea what the
code does in Explorer.
Best,
Josef