4.9 @proof の使い方
Mizar で長い article を書いていると，くりかえし Mizar チェッカーでチェックすることになります．長い article をチェックするには時間がかかります．このようなとき，既に証明が終わった定理などはチェックすることを省略することによって，Mizar チェックにかかる時間を節約することができます．
定理などのチェックするのを省略するには，proof を @proof に変えて置きます．こうすることにより，Mizar チェッカはその定理をチェックしません．
もちろん article が完成したら，すべての @proof は取り除かなければなりません．