Changeset 891 for src/ASM


Ignore:
Timestamp:
Jun 7, 2011, 4:53:53 PM (9 years ago)
Author:
campbell
Message:

Revise proofs affected by recent matita change.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVectorZ.ma

    r700 r891  
    8484    | #q #H change with ((succ one)+ (p0 p') ≤ (p0 q))
    8585      >p0_times2 >(p0_times2 q)
     86      change with (succ one * succ p' ≤ succ one * q)
    8687      @monotonic_le_times_r @IH
    8788      @le_S_S_to_le @H
Note: See TracChangeset for help on using the changeset viewer.