]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v
Initial
[helm.git] / helm / EXPORT / export_Paris_ZF / prova_Paris_ZF.v
diff --git a/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v b/helm/EXPORT/export_Paris_ZF/prova_Paris_ZF.v
new file mode 100644 (file)
index 0000000..03f5942
--- /dev/null
@@ -0,0 +1,33 @@
+Require Export Xml.
+
+Require nothing.
+Require useful.
+Require ZFbasis.
+Require axs_extensionnalite.
+Require axs_paire .
+Require axs_reunion.
+Require axs_parties.
+Require axs_comprehension.
+Require axs_remplacement.
+Require couples.
+Require applications .
+Require axs_choice.
+Require axs_fundation.
+Require ZFrelations.
+Require MSetBasis .
+
+Print XML Module Disk "examples" nothing.
+Print XML Module Disk "examples" useful.
+Print XML Module Disk "examples" ZFbasis.
+Print XML Module Disk "examples" axs_extensionnalite.
+Print XML Module Disk "examples" axs_paire .
+Print XML Module Disk "examples" axs_reunion.
+Print XML Module Disk "examples" axs_parties.
+Print XML Module Disk "examples" axs_comprehension.
+Print XML Module Disk "examples" axs_remplacement.
+Print XML Module Disk "examples" couples.
+Print XML Module Disk "examples" applications .
+Print XML Module Disk "examples" axs_choice.
+Print XML Module Disk "examples" axs_fundation.
+Print XML Module Disk "examples" ZFrelations.
+Print XML Module Disk "examples" MSetBasis .