From: Irene Schena <irene.schena@unibo.it>
Date: Mon, 19 Mar 2001 11:46:30 +0000 (+0000)
Subject: Modified Files:
X-Git-Tag: v0_1_2~62
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=945034dfb5329d074decac42bd9bdd5782748cf6;p=helm.git

Modified Files:
1) theoryobject.dtd: added theory structure
---

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>