Changeset 747 for src/utilities
 Timestamp:
 Apr 8, 2011, 2:06:46 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/Coqlib.ma
r744 r747 18 18 library. *) 19 19 20 include "utilities/binary/Z.ma".21 20 include "basics/types.ma". 22 21 include "basics/list.ma". 23 22 24 include "utilities/extralib.ma".25 23 include "ASM/Util.ma". 26 24 … … 350 348 *) 351 349 (* * Properties of powers of two. *) 352 350 (* 353 351 lemma two_power_nat_O : two_power_nat O = one. 354 352 // qed. … … 362 360 [ // 363 361  normalize #p elim p // #p' #H >(nat_succ_pos …) // 364 ] qed. 362 ] qed.*) 365 363 (* 366 364 Lemma two_p_monotone:
Note: See TracChangeset
for help on using the changeset viewer.