<?xml version="1.0" encoding="ISO-8859-1"?>
-<!DOCTYPE MathQL SYSTEM "xmathql.dtd">
+<!DOCTYPE MQLquery SYSTEM "xmathql.dtd">
-<!-- To validate: xmllint -valid -loaddtd -noout proquery.xml -->
+<!-- To validate: xmllint -valid -loaddtd -noout query.xml -->
-<MathQL>
+<MQLquery>
<Select>
<In>
- <Use>
- <Pattern arg="cic:/Coq/Init/Logic/Equality/eq.ind"/>
- <Position binder="$1"/>
- </Use>
+ <Relation name="Use">
+ <Pattern>
+ <CONST>cic:/Coq/Init/Logic/Equality/eq.ind</CONST>
+ </Pattern>
+ <Attr binder="$1"/>
+ </Relation>
</In>
- <Where rvar="result">
+ <Where rvar="@result">
<AND>
- <IS>
- <BINDER name="$1"/>
- <POSITION name="MainHypothesis"/>
- </IS>
- <IS>
- <PROPERTY name="TITLE"><RVAR name="result"/></PROPERTY>
+ <EQ>
+ <BINDER name="$1"><Rvar name="@result"/></BINDER>
+ <CONST>MainHypothesis</CONST>
+ </EQ>
+ <EQ>
+ <PROPERTY name="TITLE"><REFOF><Rvar name="@result"/></REFOF></PROPERTY>
<CONST>Uguaglianza</CONST>
- </IS>
+ </EQ>
</AND>
</Where>
</Select>
-</MathQL>
+</MQLquery>