helm/mathql/query.xml

   1 <?xml version="1.0" encoding="ISO-8859-1"?>
   2
   3 <!DOCTYPE MathQL SYSTEM "xmathql.dtd">
   4
   5 <!-- To validate: xmllint -valid -loaddtd -noout proquery.xml -->
   6
   7 <MathQL>
   8  <Select>
   9   <In>
  10    <Use>
  11     <Pattern arg="cic:/Coq/Init/Logic/Equality/eq.ind"/>
  12     <Position binder="$1"/>
  13    </Use>
  14   </In>
  15   <Where rvar="result">
  16    <AND>
  17     <IS>
  18      <BINDER name="$1"/>
  19      <POSITION name="MainHypothesis"/>
  20     </IS>
  21     <IS>
  22      <PROPERTY name="TITLE"><RVAR name="result"/></PROPERTY>
  23      <CONST>Uguaglianza</CONST>
  24     </IS>
  25    </AND>
  26   </Where>
  27  </Select>
  28 </MathQL>
  29