<!-- Third draft: May 3 2001, Irene Schena -->
<!--*****************************************************************-->
-<!-- DA AGGIUNGERE:
-CONJECTURE (teo da dim)
-EXERCISE
-EXAMPLE -->
-
<!ENTITY % cicobj SYSTEM "cicobject.dtd">
%cicobj;
<!ELEMENT ht:SECTION (%theorystructure;)>
<!ATTLIST ht:SECTION
- name CDATA #REQUIRED>
+ uri CDATA #REQUIRED>
<!ELEMENT ht:MUTUAL (ht:DEFINITION,ht:DEFINITION+)>
<!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
<!ELEMENT ht:VARIABLE (Variable)>
<!ATTLIST ht:VARIABLE
uri CDATA #REQUIRED
- as (Assumption|Hypothesis|LocalDefinition) #REQUIRED>
-
-
-
-
-
-
-
-
-
-
+ as (Assumption|Hypothesis|LocalDefinition|LocalFact) #REQUIRED>