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.Any suggestions on how to use functors from MML that require Element of NAT? Would this be the right opportunity to revise MML? The offender for me is -cut from GRAPH_2.
The revision is the best (but not the quickest) solution. Mizar enthusiasts are kindly asked for their help :). Regards, Adam Grabowski Library Committee of the Association of Mizar Users