From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 4 Apr 2004 13:44:08 +0000 (+0000)
Subject: ht:DEFINITION/Definition differentiated into
X-Git-Tag: dead_dir_walking~92
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2808f22f809adfa90fc609a10f250b788d873ffa;p=helm.git

ht:DEFINITION/Definition differentiated into
 ht:DEFINITION/Definition and
 ht:DEFINITION/InteractiveDefinition

because of an explicit request of Iris Loeb.
---

diff --git a/helm/dtd/theoryobject.dtd b/helm/dtd/theoryobject.dtd
index edd02477c..0d0d9c713 100644
--- a/helm/dtd/theoryobject.dtd
+++ b/helm/dtd/theoryobject.dtd
@@ -54,7 +54,8 @@
 <!ELEMENT ht:DEFINITION (Definition|InductiveDefinition)>
 <!ATTLIST ht:DEFINITION
           uri CDATA #REQUIRED
-          as (Definition|Inductive|CoInductive|Record) #REQUIRED>
+          as (Definition|InteractiveDefinition|Inductive|CoInductive
+             |Record) #REQUIRED>
 
 <!ELEMENT ht:THEOREM (type)>
 <!ATTLIST ht:THEOREM