Changeset 1521 for src/utilities/binary
- Timestamp:
- Nov 21, 2011, 1:06:01 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/utilities/binary/Z.ma
r1517 r1521 522 522 [ //; 523 523 | #m' >Zpred_pos_succ 524 change in ⊢ (??(??%)?); with (Zsucc (pos m'))524 change with (Zsucc (pos m')) in ⊢ (??(??%)?); 525 525 <Zpred_Zplus_neg_O >Zpred_Zsucc @refl 526 526 | #m' whd in ⊢ (??%%); >pos_compare_S_one normalize;
Note: See TracChangeset
for help on using the changeset viewer.