Revision 11

A.Removing of extended ASCII - the description is here or (more technical) here.

B. Definition of attribute Ring-like (FUNCSDOM:def 13) is canceled. We can substitute it by two attributes: right-distributive right_unital. We have removed definition of right-distributive from ALGSTR_2:def 9 to VECTSP_1:def 27 and right_unital from POLYNOM1:def 4 to VECTSP_1:def 13.
The following clusters are added:

F_Real -> right_unital (VECTSP_1)

well-unital -> right_unital (non empty multLoopStr)     (VECTSP_2)
left_unital right_unital -> well-unital (non empty multLoopStr)    (VECTSP_2)
commutative right_unital -> well-unital (non empty multLoopStr)    (VECTSP_2)

left-distributive right-distributive -> distributive     (ALGSTR_2)
    (non empty doubleLoopStr);

commutative left-distributive -> distributive     (GCD_1)
    (non empty doubleLoopStr);

C. Some registrations of clusters are repeated:
+ in RLVECT_2

definition let V be 1-sorted;
 cluster empty finite Subset of V;
end;

definition let V be non empty 1-sorted;
 cluster non empty finite Subset of V;
end;

definition let X being set;
 cluster finite Subset of X;
end;

definition
 let L be non empty 1-sorted;
 cluster finite non empty Subset of L;
end;

definition let A be set, B be non empty set;
 cluster Funcs(A,B) -> non empty;
end;

definition let X be non empty set;
 cluster Order-like Relation of X;
end;

definition let T be Tree;
 cluster -> finite Element of T;
end;

definition let n;
 cluster TOP-REAL n -> non empty;
end;

D.Generalizations:
+ In FUNCT_4: (unnecessary assumption x \in dom f)

theorem Th45:
   not x î dom g implies (f+ùg).x = f.x

   x î dom f \ dom g implies (f+ùg).x = f.x

definition
 let IT be non empty HGrStr;
 attr IT is unital means
:: GROUP_1:def 1
   ex e being Element of the carrier of IT st
        for h being Element of the carrier of IT holds
         h ù e = h & e ù h = h;
end;

 redefine mode T-Sequence of A -> Ordinal-Sequence;

E.Repeated theorems:
+ TOPREAL1:2 = PARTFUN2:17
+ MODAL_1:1 = GROUP_3:166
+ SGRAPH_1:8 = GROUP_3:166

+ WELLORD2:23, 24 are special cases of WELLORD2:26
+ SPPOL_1:1 is a special case of SPPOL_1:2.
These theorems (first ones) have been removed.

Revision 12

A. The vocabulary LEB has been changed

R_eal-like -> ext-real
R_EAL -> ExtREAL
< -> <'

B. The order of processing of Mizar articles is now different. The article NORMSP_1 is before ALGSEQ_1.

C. The repeated definitions: - INT_2, RAT_1, SCMFSA_7 from GROUP_1:

    definition let i be Integer;
      redefine func ³. i .³ -> Nat;
    end;

    definition let m, k be Nat;
      redefine func m + k -> Nat;
    end;

    definition let A, B be non empty set, f be Function of A,B,
         x be Element of A;
      redefine func f.x -> Element of B;
    end;

    definition let A be non empty Poset; let a1,a2 be Element of A;
     redefine
      pred a1 <= a2; synonym a2 >= a1;
      pred a1 < a2; synonym a2 > a1;
    end;

    definition let i be Nat, D be non empty set;
      mode Tuple of i,D is Element of i-tuples_on D;
    end;

    definition let p be Function of NAT,NAT; let n be Element of NAT;
      redefine func p.n -> Nat;
    end;

    definition let D be set, p be PartFunc of D,NAT; let n be Element of D;
      redefine func p.n -> Nat;
    end;

D. In the following definition 0 has been changed into \emptyset.

definition let f be Function, x be set;
  func f.x -> set means
:: FUNCT_1:def 4
 [x,it] î f if x î dom f otherwise it = í;
end;

E. PREPOWER The change of the definition of the functor GeoSeq, the old definitional theorem is now equal to PREPOWER:4. Functor #N became synonymous to |^ (from NEWTON).

F. Library Committee would like to reorganize the arithmetic in the Mizar Mathematical Library. In this moment, real number is an element of REAL, natural number is an element of NAT. But now we would like to introduce real number as any "set" which has "real" attribute. Because of that, two new definitions are added to ARYTM article:

definition
  redefine mode set;
  synonym number;
end;

definition let r be number;
  attr r is real means
:: ARYTM:def 2
   r î REAL;
end;

definition let x,y be Element of REAL;
  func x + y -> Element of REAL means (definiens);
end;

definition let x,y be real number;
  func x + y means (definiens);
end;

definition let x,y be real number;
  cluster x + y -> real;
end;

G. Automatic removing of obvious or repeated theorems. See here for details.

Revision 13

A. To ORDINAL1 two clusters have been added:

  cluster Ordinal-like -> epsilon-transitive epsilon-connected set;
  cluster epsilon-transitive epsilon-connected -> Ordinal-like set;

  cluster Ordinal-like -> epsilon-transitive set;

  cluster cardinal -> Ordinal-like set;

B. The following scheme from MEASURE2 is deleted as a special case of RecExD from RECDEF_1

scheme RecExFun{X()->set,D()->sigma_Field_Subset of X(),
                 A() -> (Element of D()), P[set,set,set]}:
   ex f being Function of NAT,D() st
     f.0 = A() &
     for n being Element of NAT holds P[n,f.n,f.(n+1)]
 provided
   for n being Nat for x being Element of D()
       ex y being Element of D() st P[n,x,y] and
   for n being Nat for x,y1,y2 being Element of D()
         st P[n,x,y1] & P[n,x,y2] holds y1=y2;

C. Some theorems are now canceled. See technical description for details (articles: REAL_1, REAL_2, RCOMP_1)

D. The definition POWER:def 2 looks now as follows:

definition let a,b be real number;
  func a to_power b -> real number means
  it = a #R b if a > 0,
  it = 0 if a = 0 & b > 0,
  it = 1 if a = 0 & b = 0,
  ex k st k = b & it = a #Z k if a < 0 & b is Integer;
end;

definition let n;
func 2_to_power n -> Nat equals
:: SERIES_1:def 4
2 to_power n;
end;

Revision 14

Removing of extended ASCII symbols from the MML according to propositions.

Revision 15

To be described.