Re: [mizar] Mizar 7.7.01 MML 4.68.942

[Adam Grabowski <adam@math.uwb.edu.pl>]

On Thu, 13 Jul 2006, Piotr Rudnicki wrote:

> What am I supposed to do now to make
>
> 	natural number
>
> behave as
>
> 	element of NAT
>
> without reconsidering or something equally bad?
  The solution is probably to avoid the latter 'Element of NAT'
in the Mizar source because as of now, reconsidering is necessary.
So authors are strongly encouraged to use 'Nat' or 'natural number'
in their submissions.
> Also, how does the verifier know that Element of NAT is natural?
> I cannot find a cluster to this effect.
  The point is that 'NAT' is synonymic to 'omega' - and ARYTM_3 contains
appropriate conditional cluster registration.
  Regards,
  Adam