]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/query.xml
Abst removed from the DTD.
[helm.git] / helm / mathql / query.xml
index 8e8f3792a0a13d2b5384e27462d0d89d86905bc2..e51944e8d49cd802949a73ad2009f503a0ab088c 100644 (file)
@@ -1,16 +1,16 @@
 <?xml version="1.0" encoding="ISO-8859-1"?>
 
-<!DOCTYPE MathQL SYSTEM "xmathql.dtd">
+<!DOCTYPE MQLquery SYSTEM "xmathql.dtd">
 
 <!-- To validate: xmllint -valid -loaddtd -noout query.xml -->
 
-<MathQL>
+<MQLquery>
  <Select>
   <In>
    <Use>
     <Pattern>
-     <Prefix>cic</Prefix>
-     <TokenList>
+     <PPrefix><CONST>cic</CONST></PPrefix>
+     <PBody>
       <SLASH/>
       <CONST>Coq</CONST>
       <SLASH/>
@@ -21,8 +21,8 @@
       <CONST>Equality</CONST>
       <SLASH/>
       <CONST>eq</CONST>
-     </TokenList>
-     <Extension>ind</Extension>
+     </PBody>
+     <Ext><CONST>ind</CONST></Ext>
     </Pattern>
     <Position binder="$1"/>
    </Use>
@@ -40,5 +40,5 @@
    </AND>
   </Where>
  </Select>
-</MathQL>
+</MQLquery>