--- /dev/null
+<?xml encoding="ISO-8859-1"?>
+
+<!--*****************************************************************-->
+<!-- DTD FOR THEORY OBJECTS AT LEVEL OF CIC XML FILES: -->
+<!-- First draft: May 10 2000, Claudio Sacerdoti Coen, Irene Schena -->
+<!-- Revised: February 2001, Claudio Sacerdoti Coen -->
+<!-- Revised: May 01 2001, Claudio Sacerdoti Coen -->
+<!--*****************************************************************-->
+
+<!ENTITY % mathstructure '(AXIOMS|DEFINITION|THEOREM|VARIABLES|SECTION|vernacular)*'>
+
+<!ELEMENT Theory (%mathstructure;)>
+<!ATTLIST Theory
+ uri CDATA #REQUIRED>
+
+<!ELEMENT AXIOMS (AXIOM*)>
+<!ATTLIST AXIOMS
+ as (AXIOM|PARAMETER|PARAMETERS) #REQUIRED>
+
+<!ELEMENT AXIOM EMPTY>
+<!ATTLIST AXIOM
+ uri CDATA #REQUIRED>
+
+<!ELEMENT DEFINITION EMPTY>
+<!ATTLIST DEFINITION
+ uri CDATA #REQUIRED
+ as (DEFINITION|Inductive|CoInductive|Fixpoint|CoFixpoint|Record) #REQUIRED>
+
+<!ELEMENT THEOREM EMPTY>
+<!ATTLIST THEOREM
+ uri CDATA #REQUIRED
+ as (THEOREM|LEMMA|FACT|REMARK|DECL) #REQUIRED>
+
+<!ELEMENT VARIABLES (VARIABLE*)>
+<!ATTLIST VARIABLES
+ as (VARIABLE|VARIABLES|HYPOTHESIS|HYPOTHESES|LOCAL) #REQUIRED>
+
+<!ELEMENT VARIABLE EMPTY>
+<!ATTLIST VARIABLE
+ uri CDATA #REQUIRED>
+
+<!ELEMENT SECTION (%mathstructure;)>
+<!ATTLIST SECTION
+ uri CDATA #REQUIRED>
+
+<!ELEMENT vernacular (Require|ImplicitArguments|Coercion|HintsResolve)>
+
+<!ELEMENT Require EMPTY>
+<!ATTLIST Require
+ import (EXPORT|IMPORT) #REQUIRED
+ specif (UNSPECIFIED|IMPLEMENTATION|SPECIFICATION) #REQUIRED
+ uri CDATA #REQUIRED>
+
+<!ELEMENT ImplicitArguments (EMPTY)>
+<!ATTLIST ImplicitArguments
+ status (ON) #REQUIRED>
+
+<!ELEMENT Coercion EMPTY>
+<!ATTLIST Coercion
+ kind (LOCAL|UNSPECIFIED) #REQUIRED
+ identity (IDENTITY|UNSPECIFIED) #REQUIRED
+ name CDATA #REQUIRED
+ source CDATA #REQUIRED
+ target CDATA #REQUIRED>
+
+<!ELEMENT HintsResolve (dbs,hints)>
+
+<!ELEMENT dbs (db*)>
+
+<!ELEMENT db (EMPTY)>
+<!ATTLIST db
+ name CDATA #REQUIRED>
+
+<!ELEMENT hints (hint*)>
+
+<!ELEMENT hint (EMPTY)>
+<!ATTLIST hint
+ name CDATA #REQUIRED>