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 query.xml -->
   6
   7 <MathQL>
   8  <Select>
   9   <In>
  10    <Use>
  11     <Pattern>
  12      <Prefix>cic</Prefix>
  13      <TokenList>
  14       <SLASH/>
  15       <CONST>Coq</CONST>
  16       <SLASH/>
  17       <CONST>Init</CONST>
  18       <SLASH/>
  19       <CONST>Logic</CONST>
  20       <SLASH/>
  21       <CONST>Equality</CONST>
  22       <SLASH/>
  23       <CONST>eq.ind</CONST>
  24      </TokenList>
  25     </Pattern>
  26     <Position binder="$1"/>
  27    </Use>
  28   </In>
  29   <Where rvar="result">
  30    <AND>
  31     <IS>
  32      <BINDER name="$1"/>
  33      <POSITION name="MainHypothesis"/>
  34     </IS>
  35     <IS>
  36      <PROPERTY name="TITLE"><RVAR name="result"/></PROPERTY>
  37      <CONST>Uguaglianza</CONST>
  38     </IS>
  39    </AND>
  40   </Where>
  41  </Select>
  42 </MathQL>
  43