Encoding CIC in XML: an example of theory

  <?xml version="1.0" encoding="ISO-8859-1"?>
  <!DOCTYPE Theory SYSTEM "http://localhost:8081/getdtd?url=maththeory.dtd">

  <Theory uri="cic:/coq/INIT/Logic">
   <!-- Require Export Datatypes -->
   <DEFINITION uri="True.ind"/>
   <DEFINITION uri="False.ind"/>
   <DEFINITION uri="not.con"/>
   <SECTION uri="Conjunction">
    <DEFINITION uri="and.ind"/>
    <VARIABLE uri="A.var"/>
    <VARIABLE uri="B.var"/>
    <THEOREM id="id1" uri="proj1.con"/>
    <THEOREM id="id2" uri="proj2.con"/>
   </SECTION>
   <SECTION uri="Disjunction">
    <DEFINITION uri="or.ind"/>
   </SECTION>
   <SECTION uri="Equivalence">
    <DEFINITION uri="iff.con"/>
   </SECTION>
   <DEFINITION uri="IF.con"/>
   <SECTION uri="First_order_quantifiers">
    <DEFINITION uri="ex.ind"/>
    <DEFINITION uri="ex2.ind"/>
    <DEFINITION uri="all.con"/>
   </SECTION>
   <SECTION uri="Equality">
    <DEFINITION uri="eq.ind"/>
   </SECTION>
   <SECTION uri="Logic_lemmas">
    <THEOREM id="id3" uri="absurd.con"/>
    <SECTION uri="equality">
     <VARIABLE uri="A.var"/>
     <VARIABLE uri="B.var"/>
     <VARIABLE uri="f.var"/>
     <VARIABLE uri="x.var"/>
     <VARIABLE uri="y.var"/>
     <VARIABLE uri="z.var"/>
     <THEOREM id="id4" uri="sym_eq.con"/>
     <THEOREM id="id5" uri="trans_eq.con"/>
     <THEOREM id="id6" uri="f_equal.con"/>
     <THEOREM id="id7" uri="sym_not_eq.con"/>
     <DEFINITION uri="sym_equal.con"/>
     <DEFINITION uri="sym_not_equal.con"/>
     <DEFINITION uri="trans_equal.con"/>
    </SECTION>
    <THEOREM id="id8" uri="eq_rect.con"/>
    <DEFINITION uri="eq_ind_r.con"/>
    <DEFINITION uri="eq_rec_r.con"/>
    <DEFINITION uri="eq_rect_r.con"/>
   </SECTION>
   <THEOREM id="id9" uri="f_equal2.con"/>
   <THEOREM id="id10" uri="f_equal3.con"/>
   <THEOREM id="id11" uri="f_equal4.con"/>
   <THEOREM id="id12" uri="f_equal5.con"/>
  </Theory>