Re: [mizar] Mizar 7?

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

Dear Freek,

We have changed the release number because the sytnax is different. Most
of the changes are superficial:

1. Schemes.
 1a. Private schems are not allowed anymore. So, every scheme starts
with 'scheme'
 1b. The library scheme references have the form
          from BOOLE:sch 1                                 instead
of        from Separation
   or
          from NAT_1:sch 1(A,B)                         instead
of        from Ind(A,B)
 1c. Schemes must be justified by a Proof.
2. Blocks that in a 'per cases' reasoning end with an 'end'.

3. Registration of clusters is done in a Registration Block of the form
      registration let ...;
       cluster ....
       ...
       cluster ...
       ...
     end;
4. New notation is introduced in a Notation Block of the form
     notation
       synonym .... for ....;
       antonym .... for ...;
     end;

It is almost completed. Grzegorz Bancerek implemented it, and now
Czesiek Bylinski tries to make it working.

Andrzej

Freek Wiedijk wrote:

> Hello,
>
> Today starts my course "proof assistants" in which (among
> other things) I'll try to teach Mizar.  So I downloaded the
> latest version and found that it is no longer version 6 but
> version 7!
>
> Can anyone tell me what is different that we get a new
> major version number?
>
> Freek