helm/EXPORT/exportcoq/provacoqArith.v

   1 Require Export Xml.
   2
   3 Require Arith.
   4 Require Compare.
   5 Require Compare_dec.
   6 (*Require Div.*)
   7 Require Div2.
   8 Require EqNat.
   9 Require Euclid_def.
  10 Require Euclid_proof.
  11 Require Peano_dec.
  12
  13 Print XML Module Disk "examples" Arith.
  14 Print XML Module Disk "examples" Between.
  15 Print XML Module Disk "examples" Compare.
  16 Print XML Module Disk "examples" Compare_dec.
  17 (*Print XML Module Disk "examples" Div.*)
  18 Print XML Module Disk "examples" Div2.
  19 Print XML Module Disk "examples" EqNat.
  20 Print XML Module Disk "examples" Euclid_def.
  21 Print XML Module Disk "examples" Euclid_proof.
  22 Print XML Module Disk "examples" Even.
  23 Print XML Module Disk "examples" Gt.
  24 Print XML Module Disk "examples" Le.
  25 Print XML Module Disk "examples" Lt.
  26 Print XML Module Disk "examples" Min.
  27 Print XML Module Disk "examples" Minus.
  28 Print XML Module Disk "examples" Mult.
  29 Print XML Module Disk "examples" Peano_dec.
  30 Print XML Module Disk "examples" Plus.
  31 Print XML Module Disk "examples" Wf_nat.