Re: [mizar] new vocabularies

[Artur Kornilowicz <arturk@math.uwb.edu.pl>]

Hello,

I am very sorry for my previous email. It was not finished.

I've mentioned symbols [0] and |( since during the revision they had 
caused some troubles.

[0] is widely used in induction schemes and when, for example, P[0] occurs 
in an article where vocabulary PBOOLE (containing [0]) is imported Mizar 
scanner divides P[0] into two valid tokens P and [0] and reports an error. 
A solution is to write P[0] as P[ 0 ] forceing scanner to split [0] into 
more tokens.

The same goes with |(, when |( is used like (TOP-REAL n)|(A\/B).

Best regards
Artur





On Tue, 10 Nov 2009, Artur Kornilowicz wrote:

> Dear Mizar Users,
>
> recently a quite big change of MML has been done - namely each symbol 
> introduced in an _old_ vocabulary has been moved to the _new_ vocabulary 
> named as the .miz file in which the symbol was used first.
>
> As a result of the revision vocabulary HIDDEN consists of only 3 symbols:
>
> R<>
> Rin
> Vstrict
>
>
> P[0]
> |(
>
>
> We are sorry for inconvenience. In a case of any problems with adjusting your 
> articles please ask Mizar User Service (mus@mizar.uwb.edu.pl) or me directly 
> about help.
>
> Artur