X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathql%2Fxmathql.dtd;h=96b52a22b17c4f3a2a2a155374c597026748d883;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=bcff12560dcdff29eee10b572e51561f23dac911;hpb=083c4f014ec4ed17b33fef4a01efca2c72d85b06;p=helm.git

diff --git a/helm/mathql/xmathql.dtd b/helm/mathql/xmathql.dtd
index bcff12560..96b52a22b 100644
--- a/helm/mathql/xmathql.dtd
+++ b/helm/mathql/xmathql.dtd
@@ -52,8 +52,8 @@
 
 <!-- MathQL query expression declaration -->
 
-<!ENTITY % setexpr '(Rvar|Lvar|Ref|Pattern|Select|LetIn|Relation|
-                      TypeOf|SuperTypeOf|SubTypeOf|Union|Intersect|Diff)'>
+<!ENTITY % setexpr '(Rvar|Svar|Ref|Pattern|Select|LetSIn|LetVIn|Relation|
+                     Union|Intersect|Diff)'>
 
 <!-- MathQL boolean expression declaration -->
 
@@ -61,10 +61,9 @@
 
 <!-- MathQL string-set expression declaration -->
 
-<!ENTITY % functexpr '(FUN|PROPERTY|SUPERPROPERTY|SUBPROPERTY)'>
-
-<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|%functexpr;)'>
+<!ENTITY % functexpr '(FUN|PROPERTY)'>
 
+<!ENTITY % stringsetexpr '(CONST|CONSTLIST|REFOF|BINDER|VVAR|%functexpr;)'>
 
 <!-- MathQL query top-element -->
 
@@ -86,23 +85,14 @@
 
 <!ELEMENT Select (In, Where)>
 
-<!ELEMENT LetIn (%setexpr;, Target)>
-
-<!ELEMENT Relation (%setexpr;, Attr+)>
-<!ATTLIST Relation
-          name CDATA #REQUIRED>
-
-<!ELEMENT TypeOf %setexpr;>
-<!ATTLIST TypeOf
-          binder CDATA #REQUIRED>
+<!ELEMENT LetSIn (%setexpr;, Starget)>
 
-<!ELEMENT SuperTypeOf %setexpr;>
-<!ATTLIST SuperTypeOf
-          binder CDATA #REQUIRED>
+<!ELEMENT LetVIn (%stringsetexpr;, Vtarget)>
 
-<!ELEMENT SubTypeOf %setexpr;>
-<!ATTLIST SubTypeOf
-          binder CDATA #REQUIRED>
+<!ELEMENT Relation (PName?,%setexpr;, Attr+)>
+<!ATTLIST Relation
+          name CDATA #REQUIRED
+          refine (sub|super) #IMPLIED>
 
 <!ELEMENT Union (%setexpr;, %setexpr;)>
 
@@ -118,14 +108,20 @@
 <!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 PName (CONST+)>
+
 <!-- MathQL boolean expressions -->
 
 <!ELEMENT BOOL EMPTY>
@@ -154,22 +150,16 @@
 
 <!ELEMENT REFOF %setexpr;>
 
+<!ELEMENT VVAR %stringsetexpr;>
+
 <!ELEMENT BINDER (Rvar)>
 <!ATTLIST BINDER
           name CDATA #REQUIRED>
 
-<!ELEMENT FUN (Rvar)>
+<!ELEMENT FUN %stringsetexpr;>
 <!ATTLIST FUN
           name CDATA #REQUIRED>
 
-<!ELEMENT PROPERTY (Rvar)>
+<!ELEMENT PROPERTY (Refine?,%stringsetexpr;)>
 <!ATTLIST PROPERTY
           name CDATA #REQUIRED>
-
-<!ELEMENT SUPERPROPERTY (Rvar)>
-<!ATTLIST SUPERPROPERTY
-          name CDATA #REQUIRED>
-
-<!ELEMENT SUBPROPERTY (Rvar)>
-<!ATTLIST SUBPROPERTY
-          name CDATA #REQUIRED>
\ No newline at end of file