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

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