helm/dtd/cicobject.dtd

   1 <?xml encoding="ISO-8859-1"?>
   2
   3 <!--*****************************************************************-->
   4 <!-- DTD FOR CIC OBJECTS AT LEVEL OF MATHML CONTENT:                 -->
   5 <!--  First draft: March 21, Claudio Sacerdoti Coen, Irene Schena    -->
   6 <!--*****************************************************************-->
   7
   8 <!ENTITY % mathml SYSTEM "mathml2.dtd">
   9
  10 %mathml;
  11
  12 <!ENTITY % term '(annotation|%math.qname;)'>
  13
  14 <!-- Terms: -->
  15
  16 <!ELEMENT annotation (#PCDATA|annotation|%math.qname;)*>
  17 <!ATTLIST annotation
  18           xmlns:m    CDATA #REQUIRED>
  19
  20 <!-- CIC objects: -->
  21
  22 <!ELEMENT Definition (Params,body,type)>
  23 <!ATTLIST Definition
  24           name       CDATA      #REQUIRED
  25           xmlns:m    CDATA      #REQUIRED>
  26
  27 <!ELEMENT Axiom (Params,type)>
  28 <!ATTLIST Axiom
  29           name   CDATA #REQUIRED
  30           xmlns:m    CDATA      #REQUIRED>
  31
  32 <!ELEMENT CurrentProof (Conjecture*,body,type)>
  33 <!ATTLIST CurrentProof
  34           name CDATA #REQUIRED
  35           xmlns:m    CDATA      #REQUIRED>
  36
  37 <!ELEMENT InductiveDefinition (Params,Param*,InductiveType+)>
  38 <!ATTLIST InductiveDefinition
  39           xmlns:m    CDATA      #REQUIRED>
  40
  41 <!ELEMENT Variable (type)>
  42 <!ATTLIST Variable
  43           name CDATA #REQUIRED
  44           xmlns:m    CDATA      #REQUIRED>
  45
  46 <!-- Elements used in CIC objects, which are not terms: -->
  47
  48 <!ELEMENT InductiveType (arity,Constructor*)>
  49 <!ATTLIST InductiveType
  50           name      CDATA        #REQUIRED
  51           inductive (true|false) #REQUIRED>
  52
  53 <!ELEMENT Conjecture %term;>
  54 <!ATTLIST Conjecture
  55           no NMTOKEN #REQUIRED>
  56
  57 <!ELEMENT Constructor %term;>
  58 <!ATTLIST Constructor
  59           name CDATA #REQUIRED>
  60
  61 <!ELEMENT Param %term;>
  62 <!ATTLIST Param
  63           name CDATA #REQUIRED>
  64
  65 <!ELEMENT Params (#PCDATA)*>
  66
  67 <!-- Sintactic sugar for CIC objects: -->
  68
  69 <!ELEMENT type  %term;>
  70
  71 <!ELEMENT arity %term;>
  72
  73 <!ELEMENT body  %term;>
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  93
  94
  95
  96
  97