Re: [mizar] New MML version 4.76.959

[Jesse Alama <alama@stanford.edu>]

Adam Grabowski <adam@math.uwb.edu.pl> writes:

> 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.

What is replths.txt, anyway?

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*143: No implicit qualification