Re: [mizar] Scheme for func definition with Fraenkel operator?

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

On Thu, 2 Jan 2003, Freek Wiedijk wrote:

> But I wonder now:
> 
>  (a) what _is_ the statement "Def"? (clearly it's not "Th")

You can find the exact human-legible definitional statement in MML 
Query. If you are a masochist or a computer, you can try looking at the 
*.the file in the prel directory, which contains basically the same.

Regards,
Josef