1
<?xml encoding="ISO-8859-1"?>
3
<!-- Copyright (C) 2000-2004, HELM Team -->
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. -->
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. -->
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. -->
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. -->
24
<!-- For details, see the HELM World-Wide-Web page, -->
25
<!-- http://cs.unibo.it/helm/. -->
29
<!-- Notice: the markup described in this DTD is meant to be embedded -->
30
<!-- in foreign markup (e.g. XHTML) -->
32
<!ENTITY % theorystructure
33
'(ht:AXIOM|ht:DEFINITION|ht:THEOREM|ht:VARIABLE|ht:SECTION|ht:MUTUAL)*'>
35
<!ELEMENT ht:SECTION (%theorystructure;)>
39
<!ELEMENT ht:MUTUAL (ht:DEFINITION,ht:DEFINITION+)>
43
<!ELEMENT ht:AXIOM (Axiom)>
46
as (Axiom|Declaration) #REQUIRED>
48
<!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)>
49
<!ATTLIST ht:DEFINITION
51
as (Definition|InteractiveDefinition|Inductive|CoInductive
54
<!ELEMENT ht:THEOREM (type)>
57
as (Theorem|Lemma|Corollary|Fact|Remark) #REQUIRED>
59
<!ELEMENT ht:VARIABLE (Variable)>
62
as (Assumption|Hypothesis|LocalDefinition|LocalFact) #REQUIRED>