Changeset 1521 for src/utilities


Ignore:
Timestamp:
Nov 21, 2011, 1:06:01 PM (8 years ago)
Author:
sacerdot
Message:

Syntax change in Matita: change what where => change where what.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/Z.ma

    r1517 r1521  
    522522[ //;
    523523| #m' >Zpred_pos_succ
    524     change in ⊢ (??(??%)?); with (Zsucc (pos m'))
     524    change with (Zsucc (pos m')) in ⊢ (??(??%)?);
    525525    <Zpred_Zplus_neg_O >Zpred_Zsucc @refl
    526526| #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;
Note: See TracChangeset for help on using the changeset viewer.