Changeset 747 for src/utilities


Ignore:
Timestamp:
Apr 8, 2011, 2:06:46 PM (9 years ago)
Author:
campbell
Message:

Merge the two AST files together (although some definitions still need to be
harmonised).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/Coqlib.ma

    r744 r747  
    1818    library. *)
    1919
    20 include "utilities/binary/Z.ma".
    2120include "basics/types.ma".
    2221include "basics/list.ma".
    2322
    24 include "utilities/extralib.ma".
    2523include "ASM/Util.ma".
    2624
     
    350348*)
    351349(* * Properties of powers of two. *)
    352 
     350(*
    353351lemma two_power_nat_O : two_power_nat O = one.
    354352// qed.
     
    362360[ //
    363361| normalize #p elim p // #p' #H >(nat_succ_pos …) //
    364 ] qed.
     362] qed.*)
    365363(*
    366364Lemma two_p_monotone:
Note: See TracChangeset for help on using the changeset viewer.