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</CONST>
  24      </TokenList>
  25      <Extension>ind</Extension>
  26     </Pattern>
  27     <Position binder="$1"/>
  28    </Use>
  29   </In>
  30   <Where rvar="result">
  31    <AND>
  32     <IS>
  33      <BINDER name="$1"/>
  34      <POSITION name="MainHypothesis"/>
  35     </IS>
  36     <IS>
  37      <PROPERTY name="TITLE"><RVAR name="result"/></PROPERTY>
  38      <CONST>Uguaglianza</CONST>
  39     </IS>
  40    </AND>
  41   </Where>
  42  </Select>
  43 </MathQL>
  44