]> matita.cs.unibo.it Git - helm.git/blob - helm/dtd/cicobject.dtd
Requires and Provides now fixed
[helm.git] / helm / dtd / cicobject.dtd
1 <?xml encoding="ISO-8859-1"?>
2
3 <!--*****************************************************************-->
4 <!-- DTD FOR CIC OBJECTS AT LEVEL OF MATHML CONTENT:                 -->
5 <!--  First draft: March 21, Claudio Sacerdoti Coen, Irene Schena    -->
6 <!--*****************************************************************-->
7
8 <!ENTITY % mathml SYSTEM "mathml2.dtd">
9
10 %mathml;
11
12 <!ENTITY % term '(annotation|%math.qname;)'>
13
14 <!-- Terms: -->
15
16 <!ELEMENT annotation (#PCDATA|annotation|%math.qname;)*>
17 <!ATTLIST annotation
18           xmlns:m    CDATA #REQUIRED>
19
20 <!-- CIC objects: -->
21
22 <!ELEMENT Definition (Params,body,type)>
23 <!ATTLIST Definition
24           name       CDATA      #REQUIRED
25           xmlns:m    CDATA      #REQUIRED>
26
27 <!ELEMENT Axiom (Params,type)>
28 <!ATTLIST Axiom
29           name   CDATA #REQUIRED
30           xmlns:m    CDATA      #REQUIRED>
31
32 <!ELEMENT CurrentProof (Conjecture*,body,type)>
33 <!ATTLIST CurrentProof
34           name CDATA #REQUIRED
35           xmlns:m    CDATA      #REQUIRED>
36
37 <!ELEMENT InductiveDefinition (Params,Param*,InductiveType+)>
38 <!ATTLIST InductiveDefinition
39           xmlns:m    CDATA      #REQUIRED>
40
41 <!ELEMENT Variable (type)>
42 <!ATTLIST Variable
43           name CDATA #REQUIRED
44           xmlns:m    CDATA      #REQUIRED>
45
46 <!-- Elements used in CIC objects, which are not terms: -->
47
48 <!ELEMENT InductiveType (arity,Constructor*)>
49 <!ATTLIST InductiveType
50           name      CDATA        #REQUIRED
51           inductive (true|false) #REQUIRED>
52
53 <!ELEMENT Conjecture %term;>
54 <!ATTLIST Conjecture
55           no NMTOKEN #REQUIRED>
56
57 <!ELEMENT Constructor %term;>
58 <!ATTLIST Constructor
59           name CDATA #REQUIRED>
60
61 <!ELEMENT Param %term;>
62 <!ATTLIST Param
63           name CDATA #REQUIRED>
64
65 <!ELEMENT Params (#PCDATA)*>
66
67 <!-- Sintactic sugar for CIC objects: -->
68
69 <!ELEMENT type  %term;>
70
71 <!ELEMENT arity %term;>
72
73 <!ELEMENT body  %term;>
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97