Many files added. Symbolic links missing. examples and contrib missing due

[helm.git] / helm / EXPORT / exportcoq / provacoqRelations.v

diff --git a/helm/EXPORT/exportcoq/provacoqRelations.v b/helm/EXPORT/exportcoq/provacoqRelations.v
new file mode 100644 (file)
index 0000000..c588b30
--- /dev/null
+++ b/helm/EXPORT/exportcoq/provacoqRelations.v
@@ -0,0 +1,33 @@
+Require Export Xml.
+
+Require Newman.
+Require Operators_Properties.
+Require Relation_Definitions.
+Require Relation_Operators.
+Require Relations.
+Require Rstar.
+(*Require Disjoint_Union.*)
+(*Require Inclusion.*)
+(*Require Inverse_Image.*)
+(*Require Lexicographic_Exponentiation.*)
+(*Require Lexicographic_Product.*)
+(*Require Transitive_Closure.*)
+(*Require Union.*)
+(*Require Well_Ordering.*)
+(*Require Wellfounded.*)
+
+Print XML Module Disk "examples" Newman.
+Print XML Module Disk "examples" Operators_Properties.
+Print XML Module Disk "examples" Relation_Definitions.
+Print XML Module Disk "examples" Relation_Operators.
+Print XML Module Disk "examples" Relations.
+Print XML Module Disk "examples" Rstar.
+(*Print XML Module Disk "examples/WELLFOUNDED" Disjoint_Union.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Inclusion.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Inverse_Image.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Exponentiation.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Lexicographic_Product.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Transitive_Closure.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Union.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Well_Ordering.*)
+(*Print XML Module Disk "examples/WELLFOUNDED" Wellfounded.*)