]> matita.cs.unibo.it Git - helm.git/blob - helm/dtd/cicobject.dtd
a6b6155b1f156db72c17bb8e24f67c4a88183b34
[helm.git] / helm / dtd / cicobject.dtd
1 <?xml encoding="ISO-8859-1"?>
2
3 <!-- Copyright (C) 2000, HELM Team                                     -->
4 <!--                                                                   -->
5 <!-- This file is part of HELM, an Hypertextual, Electronic            -->
6 <!-- Library of Mathematics, developed at the Computer Science         -->
7 <!-- Department, University of Bologna, Italy.                         -->
8 <!--                                                                   -->
9 <!-- HELM is free software; you can redistribute it and/or             -->
10 <!-- modify it under the terms of the GNU General Public License       -->
11 <!-- as published by the Free Software Foundation; either version 2    -->
12 <!-- of the License, or (at your option) any later version.            -->
13 <!--                                                                   -->
14 <!-- HELM is distributed in the hope that it will be useful,           -->
15 <!-- but WITHOUT ANY WARRANTY; without even the implied warranty of    -->
16 <!-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the     -->
17 <!-- GNU General Public License for more details.                      -->
18 <!--                                                                   -->
19 <!-- You should have received a copy of the GNU General Public License -->
20 <!-- along with HELM; if not, write to the Free Software               -->
21 <!-- Foundation, Inc., 59 Temple Place - Suite 330, Boston,            -->
22 <!-- MA  02111-1307, USA.                                              -->
23 <!--                                                                   -->
24 <!-- For details, see the HELM World-Wide-Web page,                    -->
25 <!-- http://cs.unibo.it/helm/.                                         -->
26
27 <!--*****************************************************************-->
28 <!-- DTD FOR CIC OBJECTS AT LEVEL OF MATHML CONTENT:                 -->
29 <!--  First draft: March 21, Claudio Sacerdoti Coen, Irene Schena    -->
30 <!--*****************************************************************-->
31
32 <!ENTITY % mathml SYSTEM "mathml2.dtd">
33
34 %mathml;
35
36 <!ENTITY % term '(annotation|%math.qname;)'>
37
38 <!-- Terms: -->
39
40 <!ELEMENT annotation (#PCDATA|annotation|%math.qname;)*>
41 <!ATTLIST annotation
42           xmlns:m    CDATA #REQUIRED>
43
44 <!-- CIC objects: -->
45
46 <!ELEMENT Definition (Params,body,type)>
47 <!ATTLIST Definition
48           name       CDATA      #REQUIRED
49           xmlns:m    CDATA      #REQUIRED>
50
51 <!ELEMENT Axiom (Params,type)>
52 <!ATTLIST Axiom
53           name   CDATA #REQUIRED
54           xmlns:m    CDATA      #REQUIRED>
55
56 <!ELEMENT CurrentProof (Conjecture*,body,type)>
57 <!ATTLIST CurrentProof
58           name CDATA #REQUIRED
59           xmlns:m    CDATA      #REQUIRED>
60
61 <!ELEMENT InductiveDefinition (Params,Param*,InductiveType+)>
62 <!ATTLIST InductiveDefinition
63           xmlns:m    CDATA      #REQUIRED>
64
65 <!ELEMENT Variable (type)>
66 <!ATTLIST Variable
67           name CDATA #REQUIRED
68           xmlns:m    CDATA      #REQUIRED>
69
70 <!-- Elements used in CIC objects, which are not terms: -->
71
72 <!ELEMENT InductiveType (arity,Constructor*)>
73 <!ATTLIST InductiveType
74           name      CDATA        #REQUIRED
75           inductive (true|false) #REQUIRED>
76
77 <!ELEMENT Conjecture %term;>
78 <!ATTLIST Conjecture
79           no NMTOKEN #REQUIRED>
80
81 <!ELEMENT Constructor %term;>
82 <!ATTLIST Constructor
83           name CDATA #REQUIRED>
84
85 <!ELEMENT Param %term;>
86 <!ATTLIST Param
87           name CDATA #REQUIRED>
88
89 <!ELEMENT Params (#PCDATA)*>
90
91 <!-- Sintactic sugar for CIC objects: -->
92
93 <!ELEMENT type  %term;>
94
95 <!ELEMENT arity %term;>
96
97 <!ELEMENT body  %term;>
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121