X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fdtd%2Ftheoryobject.dtd;h=7c20e003eff20d90f51922996a2c8030b4b342d8;hb=d42e5b087a231f25c06f370a0ae0048ddf76ca7e;hp=c8e775ac4495beecaa5e189c28b959b06efa50ed;hpb=8e1a7e55cbc7750446f0a7ab3d071190594243fb;p=helm.git

diff --git a/helm/dtd/theoryobject.dtd b/helm/dtd/theoryobject.dtd
index c8e775ac4..7c20e003e 100644
--- a/helm/dtd/theoryobject.dtd
+++ b/helm/dtd/theoryobject.dtd
@@ -27,12 +27,65 @@
 <!--*****************************************************************-->
 <!-- DTD FOR THEORY OBJECTS AT LEVEL OF MATHML CONTENT:              -->
 <!-- First draft: May 9 2000, Irene Schena                           -->
+<!-- Second draft: March 15 2001, Irene Schena                       -->
 <!--*****************************************************************-->
 
+<!-- DA AGGIUNGERE: 
+CONJECTURE (teo da dim)
+EXERCISE
+EXAMPLE -->
+
 <!ENTITY % cicobj SYSTEM "cicobject.dtd">
 
 %cicobj;
 
-<!-- THEORY section: -->
+<!ENTITY % theorystructure '(THEOREM|LEMMA|COROLLARY|AXIOM|FACT|DEFINITION|
+                           VARIABLE|SECTION)*'>
+
+<!-- Theory -->
+
+<!ELEMENT Theory (%theorystructure;)>
+<!ATTLIST Theory
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
+
+<!-- Theory Items -->
+
+<!ELEMENT THEOREM (type)>
+<!ATTLIST THEOREM
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
+
+<!ELEMENT LEMMA (type)>
+<!ATTLIST LEMMA
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
+
+<!ELEMENT COROLLARY (type)>
+<!ATTLIST COROLLARY
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
+
+<!ELEMENT AXIOM (Axiom)>
+<!ATTLIST AXIOM
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
+
+<!ELEMENT FACT (type)>
+<!ATTLIST FACT
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
+
+<!ELEMENT DEFINITION (Definition|InductiveDefinition)>
+<!ATTLIST DEFINITION
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
+
+<!ELEMENT VARIABLE (Variable)>
+<!ATTLIST VARIABLE
+          name CDATA #REQUIRED 
+          uri CDATA #REQUIRED>
 
-<!ELEMENT SECTION (SECTION|Definition|Axiom|InductiveDefinition|Variable)*>
+<!ELEMENT SECTION (%theorystructure;)>
+<!ATTLIST SECTION
+          uri CDATA #REQUIRED>