Re: [mizar] New MML version 4.76.959

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

On Fri, 19 Jan 2007, Jesse Alama wrote:

> Adam Grabowski <adam@math.uwb.edu.pl> writes:
>
> > On Fri, 19 Jan 2007, Jesse Alama wrote:
> >
> > > I had thought that 4.75.958 was the most recent MML version; I didn't
> > > even know that there was a new version.  Isn't there usually an
> > > announcement about these things?  How did you know that there was a
> > > new MML?
> >   In fact, I used to announce it; some intensive changes of the MML
> > still take place, hence my doubts about it.
>
> I understand.  Nonetheless, when a new MML is mentioned on the Mizar
> homepage and made available for download, it would be nice to know
> about it.
  Dear Jesse,
  no doubt about it - that's my fault.
> What kinds of changes are going on with the MML?
  We are still working on something which can be described
the better clustering of the library; as you probably noticed,
even if MML-searching mechanisms are available (I mean more
sophisticated than grep-based), some useful lemmas should be
gathered on the entire library, sometimes even in places you
couldn't expect. This causes enormously large "theorems" directive,
especially if you try to reuse the library as much as possible.
  To avoid this, we sometimes move such theorems (e.g. facts about
natural numbers, finite sequences etc.) from (more or less 
accidental) articles to - let's say - monographic items
to make the MML more coherent. In the next version of the system
XXREAL_1 as the another "encyclopedic" item will be established.
  After such changes however, justifications "by" can change.
  The file replths.txt contains "transition tables" from the old
library references into the new ones.
  Regards,
  Adam Grabowski