>>404
簡単な例と、

http://markun.cs.shinshu-u.ac.jp/mirror/mizar/JFM/Reqmnts/boole.html
の、BOOLEってリンクの先がMIZAR記述で、Contents (PDF format)が、自動生成されるPDF。

http://markun.cs.shinshu-u.ac.jp/mirror/mizar/JFM/mmlident.html
にこれまで証明された全てがあると思われ（自信なし）。
昔無理やりやらされた俺のファイルもあるかなwww.。


>>406
あー、オレ「普通の証明」の意味多分わかってないわ。↑が着たい違いだったらスマソ。