X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FEXPORT%2Fexport_Nijmegen_Rem%2Fexporttheories.sh;fp=helm%2FEXPORT%2Fexport_Nijmegen_Rem%2Fexporttheories.sh;h=8e64b90c5c26911ba156539244e619d4d6e0bd26;hb=88748cdbea1609de367a1e034606207d66b70508;hp=0000000000000000000000000000000000000000;hpb=40e7943e21872051f6a88cba2a1e9faa6492b6a3;p=helm.git

diff --git a/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh b/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh
new file mode 100755
index 000000000..8e64b90c5
--- /dev/null
+++ b/helm/EXPORT/export_Nijmegen_Rem/exporttheories.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+echo "Exporting theory $1";
+
+for i in Rem/*.v
+ do
+  basename=$(basename $i | sed s/\\.v//)
+  cat $i | ../mktheory.pl "Nijmegen/Rem/$basename" > \
+   examples/Nijmegen/Rem/$basename.theory.xml
+ done