1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
<?xml encoding="ISO-8859-1"?>
<!-- Copyright (C) 2000-2004, 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/. -->
<!-- Notice: the markup described in this DTD is meant to be embedded -->
<!-- in foreign markup (e.g. XHTML) -->
<!ENTITY % theorystructure
'(ht:AXIOM|ht:DEFINITION|ht:THEOREM|ht:VARIABLE|ht:SECTION|ht:MUTUAL)*'>
<!ELEMENT ht:SECTION (%theorystructure;)>
<!ATTLIST ht:SECTION
uri CDATA #REQUIRED>
<!ELEMENT ht:MUTUAL (ht:DEFINITION,ht:DEFINITION+)>
<!-- Theory Items -->
<!ELEMENT ht:AXIOM (Axiom)>
<!ATTLIST ht:AXIOM
uri CDATA #REQUIRED
as (Axiom|Declaration) #REQUIRED>
<!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)>
<!ATTLIST ht:DEFINITION
uri CDATA #REQUIRED
as (Definition|InteractiveDefinition|Inductive|CoInductive
|Record) #REQUIRED>
<!ELEMENT ht:THEOREM (type)>
<!ATTLIST ht:THEOREM
uri CDATA #REQUIRED
as (Theorem|Lemma|Corollary|Fact|Remark) #REQUIRED>
<!ELEMENT ht:VARIABLE (Variable)>
<!ATTLIST ht:VARIABLE
uri CDATA #REQUIRED
as (Assumption|Hypothesis|LocalDefinition|LocalFact) #REQUIRED>
|
