matita/dictionary-matita.xml

   1 <?xml version="1.0"?>
   2 <dictionary>
   3  <operator name="(" form="prefix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
   4  <operator name="(" form="infix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
   5  <operator name=")" form="postfix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
   6  <operator name=")" form="infix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
   7  <operator name="[" form="prefix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
   8  <operator name="[" form="infix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
   9  <operator name="]" form="postfix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
  10  <operator name="]" form="infix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
  11  <operator name="{" form="prefix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
  12  <operator name="{" form="infix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
  13  <operator name="}" form="postfix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
  14  <operator name="}" form="infix" fence="true" stretchy="false" lspace="0em" rspace="0em"/>
  15 </dictionary>