[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Re: Mizar 7.8.04 MML 4.80.962

On Sun, 25 Mar 2007, Jesse Alama wrote:


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


  Let me briefly summarize the changes in the hottest official
distribution of the Mizar system:

[snip]

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

What are the consequences of these changes for those (like me) doing
developments that use groups and fields?  I'm using the functor "1.";
should I now use "1_"?  Should I change "unital" to "well-unital"?

  Hopefully, you shouldn't change the symbol of the unity; "well-unital"
should be used instead of "unital". Note that some references have
to be changed from GROUP_1:def 5 into VECTSP_1:def 16 then, but it depends on the directives are available in your environment. I guess "identify" 
registration present at the end of VECTSP_1 will save most of your proofs
(1_F and 1.F are identified).

And where can I find the definition of a field now?
In the same place it was before, I don't think you use that from REALSET2 which was removed (well, shown equivalent), so VECTSP_1. 

Jesse

PS I'm refraining from installing the latest version because you
mentioned it has bugs.  When might the bugfix release be available?
The main bug is that some of the abstracts are broken, and some additional unnecessary comments are flagged, the database is o'k. 
  I hope it will be this Monday.
  Adam