blob: 7fe6bd362a1a2f5098e806b4c1319d7e0c74e009 [file] [log] [blame] [edit]
<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>