]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/mathql/xmathql.dtd
Modified Files:
[helm.git] / helm / mathql / xmathql.dtd
index 63c0145655b51ab407aafb1b39fe9964814adc62..3cf73eba6950cfc96a6f460d6863da83e4e3a2c1 100644 (file)
@@ -52,7 +52,7 @@
 
 <!-- MathQL query expression declaration -->
 
-<!ENTITY % setexpr '(Rvar|Svar|Ref|Pattern|Select|LetIn|Relation|
+<!ENTITY % setexpr '(Rvar|Svar|Ref|Pattern|Select|LetSIn|LetVIn|Relation|
                      Union|Intersect|Diff)'>
 
 <!-- MathQL boolean expression declaration -->
@@ -63,8 +63,7 @@
 
 <!ENTITY % functexpr '(FUN|PROPERTY)'>
 
-<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|%functexpr;)'>
-
+<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|VVAR|%functexpr;)'>
 
 <!-- MathQL query top-element -->
 
 
 <!ELEMENT Select (In, Where)>
 
-<!ELEMENT LetIn (%setexpr;, Target)>
+<!ELEMENT LetSIn (%setexpr;, Starget)>
+
+<!ELEMENT LetVIn (%stringsetexpr;, Vtarget)>
 
 <!ELEMENT Relation (Refine?,%setexpr;, Attr+)>
 <!ATTLIST Relation
-          name CDATA #REQUIRED
-          refine (sub|super) #IMPLIED>
+          name CDATA #REQUIRED>
 
 <!ELEMENT Union (%setexpr;, %setexpr;)>
 
 <!ATTLIST Where
           rvar CDATA #REQUIRED>
 
-<!ELEMENT Target %setexpr;>
-<!ATTLIST Target
+<!ELEMENT Starget %setexpr;>
+<!ATTLIST Starget
           svar CDATA #REQUIRED>
 
+<!ELEMENT Vtarget %setexpr;>
+<!ATTLIST Vtarget
+          vvar CDATA #REQUIRED>
+
 <!ELEMENT Attr EMPTY>
 <!ATTLIST Attr 
           binder CDATA #REQUIRED>
 
+<!ELEMENT Refine (SUB|SUPER|CONST+)>
+
 <!-- MathQL boolean expressions -->
 
 <!ELEMENT BOOL EMPTY>
 
 <!ELEMENT REFOF %setexpr;>
 
+<!ELEMENT VVAR %stringsetexpr;>
+
 <!ELEMENT BINDER (Rvar)>
 <!ATTLIST BINDER
           name CDATA #REQUIRED>
 <!ATTLIST FUN
           name CDATA #REQUIRED>
 
-<!ELEMENT PROPERTY %stringsetexpr;>
+<!ELEMENT PROPERTY (Refine?,%stringsetexpr;)>
 <!ATTLIST PROPERTY
-          name CDATA #REQUIRED
-          refine (sub|super) #IMPLIED>
\ No newline at end of file
+          name CDATA #REQUIRED>