]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/configuration/local/etc/helm/helm-dictionary.xml
This commit was manufactured by cvs2svn to create branch
[helm.git] / helm / configuration / local / etc / helm / helm-dictionary.xml
diff --git a/helm/configuration/local/etc/helm/helm-dictionary.xml b/helm/configuration/local/etc/helm/helm-dictionary.xml
deleted file mode 100644 (file)
index a81bb88..0000000
+++ /dev/null
@@ -1,4 +0,0 @@
-<dictionary>
- <operator name="&Union;" form="infix" stretchy="false" lspace="mediummathspace" rspace="mediummathspace"/>
- <operator name="&Intersection;" form="infix" stretchy="false" lspace="mediummathspace" rspace="mediummathspace"/>
-</dictionary>