<grammar xmlns="http://relaxng.org/ns/structure/1.0"
ns="http://relaxng.org/ns/proofsystem">
<start>
<element name="proofSystem">
<oneOrMore>
<element name="rule">
<attribute name="name"/>
<zeroOrMore>
<ref name="antecedent"/>
</zeroOrMore>
<ref name="consequent"/>
</element>
</oneOrMore>
</element>
</start>
<define name="formula">
<element name="formula">
<choice>
<ref name="judgement"/>
<ref name="expr"/>
</choice>
</element>
</define>
<define name="consequent">
<ref name="judgement"/>
</define>
<define name="antecedent">
<ref name="judgement"/>
</define>
<define name="judgement">
<choice>
<element name="judgement">
<attribute name="name"/>
<zeroOrMore>
<ref name="expr"/>
</zeroOrMore>
</element>
<element name="not">
<ref name="judgement"/>
</element>
</choice>
</define>
<define name="expr">
<choice>
<element name="var">
<attribute name="range"/>
<optional>
<attribute name="index"/>
</optional>
<optional>
<attribute name="sub"/>
</optional>
</element>
<element name="function">
<attribute name="name"/>
<zeroOrMore>
<ref name="expr"/>
</zeroOrMore>
</element>
<element name="element">
<attribute name="name"/>
<zeroOrMore>
<element name="attribute">
<attribute name="name"/>
<ref name="expr"/>
</element>
</zeroOrMore>
<optional>
<ref name="context"/>
</optional>
<zeroOrMore>
<ref name="expr"/>
</zeroOrMore>
</element>
<element name="group">
<zeroOrMore>
<ref name="expr"/>
</zeroOrMore>
</element>
<element name="string"><text/></element>
</choice>
</define>
<define name="context">
<element name="context">
<ref name="expr"/>
</element>
</define>
</grammar>
FreeBSD-CVSweb <freebsd-cvsweb@FreeBSD.org>