]> matita.cs.unibo.it Git - helm.git/commitdiff
Syntax of <attributes>...</attributes> improved to allow arguments for
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 15 Jun 2005 16:49:53 +0000 (16:49 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 15 Jun 2005 16:49:53 +0000 (16:49 +0000)
classes.

helm/dtd/cic.dtd

index 840f797f60bee29d92985f19654b303c1a7f7503..28f2804f92d7110b4f9c9b81daa4b772ea6af9fb 100644 (file)
           no  NMTOKEN #REQUIRED
           id  ID      #REQUIRED>
 
-<!ELEMENT attributes EMPTY>
-<!ATTLIST attributes
-          class (coercion|elimProp|elimCProp|elimSet|elimType|record|projection) #IMPLIED
-          generated   (true|false)  #IMPLIED>
+<!ELEMENT attributes ((class,generated?)|(generated,class?))?>
+
+<!ELEMENT generated EMPTY>
+
+<!-- the fields are allowed only when @value = "record"
+     the SORT is allowed only when @value = "elim" -->
+<!ELEMENT class (field*|SORT)>
+<!ATTLIST class
+          value (coercion|elim|record|projection) #REQUIRED>
 
 <!-- Elements used in CIC objects, which are not terms: -->