This commit was manufactured by cvs2svn to create branch 'xmltheory'.

[helm.git] / helm / dtd / maththeory.dtd

diff --git a/helm/dtd/maththeory.dtd b/helm/dtd/maththeory.dtd
deleted file mode 100644 (file)
index b05ff8f..0000000
--- a/helm/dtd/maththeory.dtd
+++ /dev/null
@@ -1,97 +0,0 @@
-<?xml encoding="ISO-8859-1"?>
-
-<!-- Copyright (C) 2000, HELM Team                                     -->
-<!--                                                                   -->
-<!-- This file is part of HELM, an Hypertextual, Electronic            -->
-<!-- Library of Mathematics, developed at the Computer Science         -->
-<!-- Department, University of Bologna, Italy.                         -->
-<!--                                                                   -->
-<!-- HELM is free software; you can redistribute it and/or             -->
-<!-- modify it under the terms of the GNU General Public License       -->
-<!-- as published by the Free Software Foundation; either version 2    -->
-<!-- of the License, or (at your option) any later version.            -->
-<!--                                                                   -->
-<!-- HELM is distributed in the hope that it will be useful,           -->
-<!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
-<!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
-<!-- GNU General Public License for more details.                      -->
-<!--                                                                   -->
-<!-- You should have received a copy of the GNU General Public License -->
-<!-- along with HELM; if not, write to the Free Software               -->
-<!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
-<!-- MA  02111-1307, USA.                                              -->
-<!--                                                                   -->
-<!-- For details, see the HELM World-Wide-Web page,                    -->
-<!-- http://cs.unibo.it/helm/.                                         -->
-
-<!--*****************************************************************-->
-<!-- DTD FOR THEORY OBJECTS AT LEVEL OF CIC XML FILES:               -->
-<!-- First draft: May 10 2000, Claudio Sacerdoti Coen, Irene Schena  -->
-<!--*****************************************************************-->
-
-<!-- manca il semplice enunciato -->
-<!-- mancano i link ad altre teorie? (corrispondenti a Require?) -->
-<!-- una teoria "vuota" e' una teoria? -->
-<!ENTITY % mathstructure '(THEOREM|LEMMA|COROLLARY|AXIOM|FACT|DEFINITION|
-                           VARIABLE|SECTION)*'>
-
-<!ELEMENT Theory (%mathstructure;)>
-<!ATTLIST Theory
-          uri CDATA #REQUIRED>
-
-<!ELEMENT THEOREM EMPTY>
-<!ATTLIST THEOREM
-          id  IDREF #REQUIRED
-          uri CDATA #REQUIRED>
-
-<!ELEMENT LEMMA EMPTY>
-<!ATTLIST LEMMA
-          id     IDREF #REQUIRED
-          uri    CDATA #REQUIRED 
-          target IDREF #REQUIRED>
-
-<!ELEMENT COROLLARY EMPTY>
-<!ATTLIST COROLLARY
-          id     IDREF #REQUIRED
-          uri    CDATA #REQUIRED 
-          target IDREF #REQUIRED>
-
-<!ELEMENT AXIOM EMPTY>
-<!ATTLIST AXIOM
-          id  IDREF #REQUIRED
-          uri CDATA #REQUIRED>
-
-<!ELEMENT FACT EMPTY>
-<!ATTLIST FACT
-          id  IDREF #REQUIRED
-          uri CDATA #REQUIRED>
-
-<!ELEMENT DEFINITION EMPTY>
-<!ATTLIST DEFINITION
-          uri CDATA #REQUIRED>
-
-<!ELEMENT VARIABLE EMPTY>
-<!ATTLIST VARIABLE
-          uri CDATA #REQUIRED>
-
-<!ELEMENT SECTION (%mathstructure;)>
-<!ATTLIST SECTION
-          uri CDATA #REQUIRED>
-
-<!--
- VINCOLI DI VALIDITA' NON ESPRIMIBILI NEL DTD:
-  Siano V una variabile e T,T' due fatti/definizioni/teoremi/lemmi/corollari
-
-   - per visualizzare T dipendente da T' dove T' e T sono definiti nella stessa
-     (da definirsi) teoria/sezione, debbo visualizzare anche T'? 
-   - per visualizzare T dipendente da T' dove anche T' e' visualizzato, debbo
-     visualizzare T necessariamente dopo T'?
-   + consistenza fra la dipendenza dei lemmi e dei corollari dal loro target
-     e quella effettiva data dal livello degli oggetti
-   + tutte le URI debbono essere relative e discendenti (= non contenti "..")
-   +? ogni lemma deve precedere (strettamente?) il suo target
-   +? ogni corollario deve seguire (strettamente?) il suo target
-   + se T/V dipende da V, allora V deve essere visualizzata 
-   + se T/V dipende da V, allora V deve essere visualizzata prima di T
-    PROBLEMA: NON ABBIAMO INFORMAZIONI SULLA DIPENDENZA DI V DA V!!!
--->