helm/mathql/query.xml

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