[mizar] @; and @by

[Piotr Rudnicki <piotr@cs.ualberta.ca>]

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