]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/EXPORT/exportcoq/provacoqLists.v
Many files added. Symbolic links missing. examples and contrib missing due
[helm.git] / helm / EXPORT / exportcoq / provacoqLists.v
diff --git a/helm/EXPORT/exportcoq/provacoqLists.v b/helm/EXPORT/exportcoq/provacoqLists.v
new file mode 100644 (file)
index 0000000..91b74ef
--- /dev/null
@@ -0,0 +1,15 @@
+Require Export Xml.
+
+Require List.
+Require ListSet.
+Require PolyList.
+(*Require PolyListSyntax.*)
+Require Streams.
+Require TheoryList.
+
+Print XML Module Disk "examples" List.
+Print XML Module Disk "examples" ListSet.
+Print XML Module Disk "examples" PolyList.
+(*Print XML Module Disk "examples" PolyListSyntax.*)
+Print XML Module Disk "examples" Streams.
+Print XML Module Disk "examples" TheoryList.