[mizar] New MML version 4.76.959

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

On Fri, 19 Jan 2007, Jesse Alama wrote:

> Josef Urban <urban@ktilinux.ms.mff.cuni.cz> writes:
>
> > the new HTML is browsable at
> > http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.76.959/ , and
> > downloadable at
> > http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.76.959.tar.gz
> > (unpacks to 1.2GB).
>
> 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.
  There is a new MML version available under our usual ftp address,
still there are old binaries (7.8.03), but the changes in the library
are rather big. First of all, if you use the type of "natural number" or
"Nat" which is synonymous, you can discover the change of the structure
of files in which it was introduced (NAT_D is new).
Now the usual operations (as div, mod, also divisibility) are unified for
both integer and natural numbers, and basic definitions together with
properties are stored in NAT_D.
  NAT_1 was reorganized, canceled theorems are now removed so the care
with numbers of theorems (if you had some in your mind) is advised.
The file replths.txt in the distribution should help a lot.
  The version which is "official" at the moment is usually also announced
at the top of the home page of the Mizar system.
  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users