Changeset 1521 for src/ASM/BitVector.ma


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/ASM/BitVector.ma

    r1516 r1521  
    184184    #hd' * #tl' #jmeq >jmeq in h;
    185185    #new_h
    186     change in new_h; with ((andb ? ?) = ?);
     186    change with ((andb ? ?) = ?) in new_h;
    187187    cases(conjunction_true … new_h)
    188188    #eq_heads #eq_tails
     
    190190    cases(eq_b_eq … eq_heads)
    191191    whd in eq_tails:(??(?????(%))?);
    192     change in eq_tails; with (eq_bv ??? = ?);
     192    change with (eq_bv ??? = ?) in eq_tails;
    193193    <(ih tl') //
    194194  ]
Note: See TracChangeset for help on using the changeset viewer.