helm/EXPORT/exportcoq/provacoqSets.v

   1 Require Export Xml.
   2
   3 Require Classical_sets.
   4 Require Constructive_sets.
   5 Require Cpo.
   6 Require Ensembles.
   7 Require Finite_sets.
   8 Require Finite_sets_facts.
   9 Require Image.
  10 Require Infinite_sets.
  11 Require Integers.
  12 Require Multiset.
  13 Require Partial_Order.
  14 Require Permut.
  15 (*Require CSCPermut.*)
  16 Require Powerset.
  17 Require Powerset_Classical_facts.
  18 Require Powerset_facts.
  19 Require Relations_1.
  20 Require Relations_1_facts.
  21 Require Relations_2.
  22 Require Relations_2_facts.
  23 Require Relations_3.
  24 Require Relations_3_facts.
  25 Require Uniset.
  26
  27 Print XML Module Disk "examples" Classical_sets.
  28 Print XML Module Disk "examples" Constructive_sets.
  29 Print XML Module Disk "examples" Cpo.
  30 Print XML Module Disk "examples" Ensembles.
  31 Print XML Module Disk "examples" Finite_sets.
  32 Print XML Module Disk "examples" Finite_sets_facts.
  33 Print XML Module Disk "examples" Image.
  34 Print XML Module Disk "examples" Infinite_sets.
  35 Print XML Module Disk "examples" Integers.
  36 Print XML Module Disk "examples" Multiset.
  37 Print XML Module Disk "examples" Partial_Order.
  38 Print XML Module Disk "examples" Permut.
  39 Print XML Module Disk "examples" Powerset.
  40 Print XML Module Disk "examples" Powerset_Classical_facts.
  41 Print XML Module Disk "examples" Powerset_facts.
  42 Print XML Module Disk "examples" Relations_1.
  43 Print XML Module Disk "examples" Relations_1_facts.
  44 Print XML Module Disk "examples" Relations_2.
  45 Print XML Module Disk "examples" Relations_2_facts.
  46 Print XML Module Disk "examples" Relations_3.
  47 Print XML Module Disk "examples" Relations_3_facts.
  48 Print XML Module Disk "examples" Uniset.