matita.cs.unibo.it Git - helm.git/blob - helm/configuration/local/etc/helm/helm-dictionary.xml

]> matita.cs.unibo.it Git - helm.git/blob - helm/configuration/local/etc/helm/helm-dictionary.xml

projects / helm.git / blob

summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD

[helm.git] / helm / configuration / local / etc / helm / helm-dictionary.xml

 <dictionary>
  <operator name="&Union;" form="infix" stretchy="false" lspace="mediummathspace" rspace="mediummathspace"/>
  <operator name="&Intersection;" form="infix" stretchy="false" lspace="mediummathspace" rspace="mediummathspace"/>
 </dictionary>

Unnamed repository; edit this file 'description' to name the repository.