helm/EXPORT/exportcoq/provacoqRelations.v

   1 Require Export Xml.
   2
   3 Require Newman.
   4 Require Operators_Properties.
   5 Require Relation_Definitions.
   6 Require Relation_Operators.
   7 Require Relations.
   8 Require Rstar.
   9 (*Require Disjoint_Union.*)
  10 (*Require Inclusion.*)
  11 (*Require Inverse_Image.*)
  12 (*Require Lexicographic_Exponentiation.*)
  13 (*Require Lexicographic_Product.*)
  14 (*Require Transitive_Closure.*)
  15 (*Require Union.*)
  16 (*Require Well_Ordering.*)
  17 (*Require Wellfounded.*)
  18
  19 Print XML Module Disk "examples" Newman.
  20 Print XML Module Disk "examples" Operators_Properties.
  21 Print XML Module Disk "examples" Relation_Definitions.
  22 Print XML Module Disk "examples" Relation_Operators.
  23 Print XML Module Disk "examples" Relations.
  24 Print XML Module Disk "examples" Rstar.
  25 (*Print XML Module Disk "examples/WELLFOUNDED" Disjoint_Union.*)
  26 (*Print XML Module Disk "examples/WELLFOUNDED" Inclusion.*)
  27 (*Print XML Module Disk "examples/WELLFOUNDED" Inverse_Image.*)
  28 (*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Exponentiation.*)
  29 (*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Product.*)
  30 (*Print XML Module Disk "examples/WELLFOUNDED" Transitive_Closure.*)
  31 (*Print XML Module Disk "examples/WELLFOUNDED" Union.*)
  32 (*Print XML Module Disk "examples/WELLFOUNDED" Well_Ordering.*)
  33 (*Print XML Module Disk "examples/WELLFOUNDED" Wellfounded.*)