[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
[mizar] Re: Mizar 7.8.04 MML 4.80.962
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.
> - 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.
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"?
And where can I find the definition of a field now?
Jesse
PS I'm refraining from installing the latest version because you
mentioned it has bugs. When might the bugfix release be available?
--
Jesse Alama (alama@stanford.edu)
*116: Invalid "qua" (http://www.mizar.org)