Modified Files:

[helm.git] / helm / mathql / query.xml

diff --git a/helm/mathql/query.xml b/helm/mathql/query.xml
new file mode 100644 (file)
index 0000000..68fb999
--- /dev/null
+++ b/helm/mathql/query.xml
@@ -0,0 +1,29 @@
+<?xml version="1.0" encoding="ISO-8859-1"?>
+
+<!DOCTYPE MathQL SYSTEM "xmathql.dtd">
+
+<!-- To validate: xmllint -valid -loaddtd -noout proquery.xml -->
+
+<MathQL>
+ <Select>
+  <In>
+   <Use>
+    <Pattern arg="cic:/Coq/Init/Logic/Equality/eq.ind"/>
+    <Position binder="$1"/>
+   </Use>
+  </In>
+  <Where rvar="result">
+   <AND>
+    <IS>
+     <BINDER name="$1"/>
+     <POSITION name="MainHypothesis"/>
+    </IS>
+    <IS>
+     <PROPERTY name="TITLE"><RVAR name="result"/></PROPERTY>
+     <CONST>Uguaglianza</CONST>
+    </IS>
+   </AND>
+  </Where>
+ </Select>
+</MathQL>
+