<?xml version="1.0" encoding="iso-8859-1"?>
<!-- $Id: spec.rng,v 1.3 2001/10/23 05:54:24 jjc Exp $ -->
<grammar xmlns="http://relaxng.org/ns/structure/1.0"
         datatypeLibrary="http://www.w3.org/2001/XMLSchema-datatypes"
          xmlns:p="http://relaxng.org/ns/proofsystem">

<start>
  <grammar>
    <include href="docbook.rng"/>
    <define name="synop.class" combine="choice">
      <choice>
        <parentRef name="rngref"/>
        <parentRef name="grammarref"/>
        <grammar>
          <include href="proofsystem.rng"/>
          <start combine="choice">
            <ref name="formula"/>
          </start>
        </grammar>
      </choice>
    </define>
    <define name="tech.char.class" combine="choice">
      <parentRef name="terms"/>
    </define>
  </grammar>
</start>

<define name="rngref">
  <element name="rngref">
    <attribute name="src">
      <data type="anyURI"/>
    </attribute>
  </element>
</define>

<define name="grammarref">
  <element name="grammarref">
    <attribute name="src">
      <data type="anyURI"/>
    </attribute>
  </element>
</define>

<define name="terms">
  <grammar>
     <include href="proofsystem.rng">
       <start>
         <choice>
           <ref name="expr"/>
           <ref name="judgement"/>
           <ref name="context"/>
         </choice>
       </start>
     </include>
  </grammar>
</define>

</grammar>