Re: [mizar] Re: Mizar 7.8.04 MML 4.80.962

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

On Sat, 24 Mar 2007, Freek Wiedijk wrote:

> Piotr:
>
> > > >   this is to inform you that the new release of the Mizar Mathematical
> > > > Library (4.80.962) is now available together with the system binaries
> > > > (ver. 7.8.04) for all supported platforms. Underlying links can be
> > > > find
> > > > on our main home page (http://mizar.uwb.edu.pl and http://mizar.org).
> > > >   If you encounter any troubles with the use of this brand new version,
> > > > you can contact mml or mus at mizar.uwb.edu.pl.
> > >
> > > What's new in this version?
> >
> > While awaiting an answer I invented several working hypotheses:
>
> Well, the version number went from 7.8.03 to 7.8.04, which
> looks rather minor to me.  So my guess for the answer is:
>
> > 	- Something is new but so small that it is not worthwhile
> >          talking about.
>
> Of course you also get three more articles in the MML.  And
> maybe the already existing articles were revised too, who knows?
  Dear All,
  and this is the winner, exactly! ;)
  Let me briefly summarize the changes in the hottest official
distribution of the Mizar system:

- The basic change in the Mizar sources which enforced
  the revision is that local definitions (objects introduced
  mainly by the "set" construct) are prohibited now in the
  exportable items. This was used extensively in the SCM series,
  unfortunately, due to the change the readability of these
  articles is much smaller.
- There is no agreement which approach is better: (let me describe
  this based on the definition of a group) - to define the unity
  of a group as the selector of the underlying structure possessing
  the appropriate properties (the latter via "attribute" definition),
  or to introduce it by an adjective without any additional selector.
  The earlier approach is represented by "well-unital" adjective (and
  the unity is denoted by 1.F for a field F), the latter - by
  "unital" one (1_F). The change, done by Andrzej Trybulec consisted
  mainly in replacing "unital" with "well-unital" and "1." with "1_"
  (for "well-unital" these are equivalent notions). I am not sure if
  it's right because as I remember some five years ago we did exactly
  the opposite - but the "identify" construction wasn't available those
  days.
- STRUCT_0 was expanded; ZeroStr and OneStr, with additional
  "ZeroF" and "OneF" selectors instead of original "Zero" and
  "unity". Also the attribute "degenerated" (for structures
  having the zero and the unity equal) was moved there.
- The article with MML identifier REALSET2 was practically
  redesigned. The reason was that the definitions of a field
  and of an Abelian group which are also present in VECTSP_1
  had practically the same meaning - although the equivalence
  between both approaches was not shown. Now duplicate
  definitions are removed.
- We still work to divide the MML into the classical and
  abstract part, so the ordering of articles reflected in
  mml.lar file continuously changes; these changes are
  rather minor, we move some auxiliary definitions and
  lemmas from articles which are - so to say - accidental
  to more appropriate ones. Here the changes are rather
  significant but an ordinary Mizar user probably won't
  notice it (e.g. scheme of the existence of functions from ZFREFLE1
  in now in CLASSES1, or the functor IFEQ which was in CQC_LANG
  is now in FUNCOP_1).

Of course, there are three new articles:

- BCIALG_1
    Several Classes of BCI-algebras and Their Properties
     by Yuzhong Ding
- FLANG_1
    Formal Languages -- Concatenation and Closure
     by Micha{\l} Trybulec
- MATRIX11
    Basic Properties of Determinants of Square Matrices over a Field
     by Karol P\c{a}k

  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users