Initial

[helm.git] / helm / EXPORT / export_Rocq_SHUFFLE / prova_Rocq_SHUFFLE.v

diff --git a/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v b/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v
new file mode 100644 (file)
index 0000000..1b17a93
--- /dev/null
+++ b/helm/EXPORT/export_Rocq_SHUFFLE/prova_Rocq_SHUFFLE.v
@@ -0,0 +1,16 @@
+Require Export Xml.
+
+Require Alternate.
+Require Gilbreath.
+Require Opposite.
+Require Paired.
+Require Shuffle.
+Require Words.
+
+
+Print XML Module Disk "examples" Alternate.
+Print XML Module Disk "examples" Gilbreath.
+Print XML Module Disk "examples" Opposite.
+Print XML Module Disk "examples" Paired.
+Print XML Module Disk "examples" Shuffle.
+Print XML Module Disk "examples" Words.