]> matita.cs.unibo.it Git - helm.git/blob - helm/xmltheory/maththeory.dtd
Stupid typo fixed.
[helm.git] / 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>