helm/EXPORT/exportcoq/provacoqcontribOmega.v

   1 Require Export Xml.
   2
   3 Require Omega.
   4 Require Zlogarithm.
   5 Require OmegaSyntax.
   6 Require Zpower.
   7
   8 Print XML Module Disk "examples" Omega.
   9 Print XML Module Disk "examples" Zlogarithm.
  10 Print XML Module Disk "examples" OmegaSyntax.
  11 Print XML Module Disk "examples" Zpower.