5. Miscellaneous editing

5.1 Proof checking

C-c C-d

mizar-hide-proofs

Command: mizar-hide-proofs &optional beg end remove

Put @ before all proof keywords between beg and end to disable checking.
With prefix (C-u, which sets remove non-nil) remove them instead of adding, to enable proof checking again.

This function is available also from menu, to make it easy to apply it in reverse mode and on complete buffer.

5.2 Then placement

Command: mizar-move-then &optional beg end reverse

Change the placement of the 'then' keyword between beg and end.
With prefix (reverse non-nil) move from the end of lines to beginnings, otherwise from beginnings of lines to ends. This is a flamewar-resolving hack.

This function is available also from menu, to make it easy to apply it in reverse mode and on complete buffer.