helm/xmltheory/maththeory.dtd

   1 <?xml encoding="ISO-8859-1"?>
   2
   3 <!--*****************************************************************-->
   4 <!-- DTD FOR THEORY OBJECTS AT LEVEL OF CIC XML FILES:               -->
   5 <!-- First draft: May 10 2000, Claudio Sacerdoti Coen, Irene Schena  -->
   6 <!-- Revised: February 2001, Claudio Sacerdoti Coen                  -->
   7 <!-- Revised: May 01 2001, Claudio Sacerdoti Coen                    -->
   8 <!--*****************************************************************-->
   9
  10 <!ENTITY % mathstructure '(AXIOMS|DEFINITION|THEOREM|VARIABLES|SECTION|vernacular)*'>
  11
  12 <!ELEMENT Theory (%mathstructure;)>
  13 <!ATTLIST Theory
  14           uri CDATA #REQUIRED>
  15
  16 <!ELEMENT AXIOMS (AXIOM*)>
  17 <!ATTLIST AXIOMS
  18           as (AXIOM|PARAMETER|PARAMETERS) #REQUIRED>
  19
  20 <!ELEMENT AXIOM EMPTY>
  21 <!ATTLIST AXIOM
  22           uri CDATA #REQUIRED>
  23
  24 <!ELEMENT DEFINITION EMPTY>
  25 <!ATTLIST DEFINITION
  26           uri CDATA #REQUIRED
  27           as (DEFINITION|Inductive|CoInductive|Fixpoint|CoFixpoint|Record) #REQUIRED>
  28
  29 <!ELEMENT THEOREM EMPTY>
  30 <!ATTLIST THEOREM
  31           uri CDATA #REQUIRED
  32           as (THEOREM|LEMMA|FACT|REMARK|DECL) #REQUIRED>
  33
  34 <!ELEMENT VARIABLES (VARIABLE*)>
  35 <!ATTLIST VARIABLES
  36           as (VARIABLE|VARIABLES|HYPOTHESIS|HYPOTHESES|LOCAL) #REQUIRED>
  37
  38 <!ELEMENT VARIABLE EMPTY>
  39 <!ATTLIST VARIABLE
  40           uri CDATA #REQUIRED>
  41
  42 <!ELEMENT SECTION (%mathstructure;)>
  43 <!ATTLIST SECTION
  44           uri CDATA #REQUIRED>
  45
  46 <!ELEMENT vernacular (Require|ImplicitArguments|Coercion|HintsResolve)>
  47
  48 <!ELEMENT Require EMPTY>
  49 <!ATTLIST Require
  50           import (EXPORT|IMPORT)                             #REQUIRED
  51           specif (UNSPECIFIED|IMPLEMENTATION|SPECIFICATION)  #REQUIRED
  52           uri    CDATA                                       #REQUIRED>
  53
  54 <!ELEMENT ImplicitArguments (EMPTY)>
  55 <!ATTLIST ImplicitArguments
  56           status (ON) #REQUIRED>
  57
  58 <!ELEMENT Coercion EMPTY>
  59 <!ATTLIST Coercion
  60           kind     (LOCAL|UNSPECIFIED)    #REQUIRED
  61           identity (IDENTITY|UNSPECIFIED) #REQUIRED
  62           name     CDATA                  #REQUIRED
  63           source   CDATA                  #REQUIRED
  64           target   CDATA                  #REQUIRED>
  65
  66 <!ELEMENT HintsResolve (dbs,hints)>
  67
  68 <!ELEMENT dbs (db*)>
  69
  70 <!ELEMENT db (EMPTY)>
  71 <!ATTLIST db
  72           name CDATA #REQUIRED>
  73
  74 <!ELEMENT hints (hint*)>
  75
  76 <!ELEMENT hint (EMPTY)>
  77 <!ATTLIST hint
  78           name CDATA #REQUIRED>