]> matita.cs.unibo.it Git - helm.git/blobdiff - mathql/query.xml
moved mathql/ under software/
[helm.git] / mathql / query.xml
diff --git a/mathql/query.xml b/mathql/query.xml
new file mode 100644 (file)
index 0000000..4efca73
--- /dev/null
@@ -0,0 +1,31 @@
+<?xml version="1.0" encoding="ISO-8859-1"?>
+
+<!DOCTYPE MQLquery SYSTEM "xmathql.dtd">
+
+<!-- To validate: xmllint -valid -loaddtd -noout query.xml -->
+
+<MQLquery>
+ <Select>
+  <In>
+   <Relation name="Use">
+    <Pattern>
+     <CONST>cic:/Coq/Init/Logic/Equality/eq.ind</CONST>
+    </Pattern>
+    <Attr binder="$1"/>
+   </Relation>
+  </In>
+  <Where rvar="@result">
+   <AND>
+    <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>
+    </EQ>
+   </AND>
+  </Where>
+ </Select>
+</MQLquery>
+