@; and @by

Hi,

Analogously to @proof, I propose to add to Mizar also a possibility to
switch-off checking of simple justifications by using @; and @by.

Reason: inside a longer proof I frequently have several places which are on
the 'frontier' and I do not want them being checked and marked with the *4
error.

What I do now is add @proof end; in such cases, but I cannot do it in steps
where proofs are not allowed and then 'contradiction @proof end; then' does
the trick.

@by is needed for cases where I want to switch-off checking of a
long-running step.

All this can be done with pragmas.  There was some discussion of pragmas
some time ago but I do not see any documentation/info about it.

Cheers,

-- 
Piotr Rudnicki
http://www.cs.ualberta.ca/~piotr