Re: [mizar] How to properly do inductive sets in Mizar?

[Freek Wiedijk <freek@cs.kun.nl>]

Hi Josef,

>Unfortunately, the proof of Knaster is not too long, so
>grepping e.g. for all theorems from the article KNASTER
>might be necessary too.

% mmlgrep -l KNASTER:
/usr/local/lib/mizar/mml/abian.miz
/usr/local/lib/mizar/mml/amistd_2.miz
/usr/local/lib/mizar/mml/hilbert3.miz
% 

So that doesn't seem to help either.  Those articles don't
seem (from their subjects) to be about inductive sets.  At
least they don't define any schemes.

>Grep is not bad,

The main problem for me is the crossing of lines.  It would
be useful to have a version of the MML abstracts in which
each statement is printed in exactly one long line, and using
some standard style of spacing.

Freek