Re: [mizar] Private DB

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

Hi Josef,

>It seems to me that once an article is submitted to MML (and published in 
>FM, and all the glory belonging to the author properly recorded), it 
>really should be "dismantled" into pieces which are put into proper parts 
>of the MML structure.

I agree!  Or, a little bit weaker version of this: the author
can be asked to divide his/her article into two parts, the first
of which is "lemmas that should have been elsewhere" and
the second of which he/she really would like to be kept together.

My articles generally fall apart in two halves like that.

Freek