X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fxmltheory%2Fmaththeory.dtd;fp=helm%2Fxmltheory%2Fmaththeory.dtd;h=f010b65003912a4fd9b115d264fb6d429f11bfc6;hb=9a3551a665bcc68c9e2d4f7a220e4dfabad3fde1;hp=0000000000000000000000000000000000000000;hpb=f0ba4a2e4c476fa162e4bf976b323cbfb492dec5;p=helm.git

diff --git a/helm/xmltheory/maththeory.dtd b/helm/xmltheory/maththeory.dtd
new file mode 100644
index 000000000..f010b6500
--- /dev/null
+++ b/helm/xmltheory/maththeory.dtd
@@ -0,0 +1,78 @@
+<?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>