Re: [mizar] Mizar 7.7.01 MML 4.68.942

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

Hi,

What am I supposed to do now to make

	natural number

behave as 

	element of NAT 

without reconsidering or something equally bad?

Also, how does the verifier know that Element of NAT is natural?
I cannot find a cluster to this effect.

PR






On Thu, Jul 13, 2006 at 11:40:31AM +0200, Adam Grabowski wrote:
>   Dear Mizar Users,
>   this is to inform you that the new release of the Mizar Mathematical
> Library (4.68.942) is now available together with the system binaries 
> (ver. 7.7.01) for all supported platforms. Underlying links can be find
> on our main home page (http://mizar.uwb.edu.pl and http://mizar.org).
>   As you could know already, the use of 'natural number' ('real number')
> over 'Element of NAT' ('Element of REAL', resp.) is preferred. To shorten
> the notation we change the meaning of the 'Nat' mode from 'Element of NAT'
> into 'natural number'. If you encounter some new errors, adding 'XCMPLX_0'
> to 'notations' and 'NAT_1' to 'registrations' directive in your 
> environment declaration will probably be helpful.
>   Note that every time you would like to submit your Mizar article
> for inclusion in the Mizar Mathematical Library you should check
> if your article do not produce any errors under the latest official
> release of the Mizar system. Otherwise, the submission will be returned
> to its author and hence will not be subject for the review process.
>   Older submissions will be revised by the Library Committee.
>   Regards,
>   Adam Grabowski
>   Library Committee of the Association of Mizar Users

-- 
Piotr Rudnicki        CompSci, University of Alberta, Edmonton, Canada
                      http://web.cs.ualberta.ca/~piotr