+++ /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>