src/Pure/Tools/isabelle.xsd

Context.display_names;

<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">

<xsd:element name="class">
  <xsd:complexType>
    <xsd:attribute name="name" type="xsd:string" use="required"/>
  </xsd:complexType>
</xsd:element>

<xsd:element name="type">
  <xsd:complexType>
    <xsd:group ref="typeGroup"/>
  </xsd:complexType>
</xsd:element>

<xsd:element name="types">
  <xsd:complexType>
    <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
  </xsd:complexType>
</xsd:element>

<xsd:group name="typeGroup">
  <xsd:choice>
    <xsd:element name="TVar">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
        <xsd:attribute name="index" type="xsd:integer"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="TFree">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Type">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
  </xsd:choice>
</xsd:group>

<xsd:element name="term">
  <xsd:complexType>
    <xsd:group ref="termGroup"/>
  </xsd:complexType>
</xsd:element>

<xsd:group name="termGroup">
  <xsd:choice>
    <xsd:element name="Var">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="typeGroup"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
        <xsd:attribute name="index" type="xsd:integer"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Free">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="typeGroup"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Const">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="typeGroup"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Bound">
      <xsd:complexType>
        <xsd:attribute name="index" type="xsd:integer" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="App">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="termGroup"/>
          <xsd:group ref="termGroup"/>
        </xsd:sequence>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Abs">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="typeGroup"/>
          <xsd:group ref="termGroup"/>
        </xsd:sequence>
        <xsd:attribute name="vname" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
  </xsd:choice>
</xsd:group>

<xsd:element name="proof">
  <xsd:complexType>
    <xsd:group ref="proofGroup"/>
  </xsd:complexType>
</xsd:element>

<xsd:group name="proofGroup">
  <xsd:choice>
    <xsd:element name="PThm">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="termGroup" minOccurs="0"/>
          <xsd:element ref="types" minOccurs="0"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="PAxm">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="termGroup" minOccurs="0"/>
          <xsd:element ref="types" minOccurs="0"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Oracle">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="termGroup"/>
          <xsd:element ref="types" minOccurs="0"/>
        </xsd:sequence>
        <xsd:attribute name="name" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="PBound">
      <xsd:complexType>
        <xsd:attribute name="index" type="xsd:integer" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Appt">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="proofGroup"/>
          <xsd:group ref="termGroup" minOccurs="0"/>
        </xsd:sequence>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="AppP">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="proofGroup"/>
          <xsd:group ref="proofGroup"/>
        </xsd:sequence>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Abst">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="typeGroup" minOccurs="0"/>
          <xsd:group ref="proofGroup"/>
        </xsd:sequence>
        <xsd:attribute name="vname" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="AbsP">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="termGroup" minOccurs="0"/>
          <xsd:group ref="proofGroup"/>
        </xsd:sequence>
        <xsd:attribute name="vname" type="xsd:string" use="required"/>
      </xsd:complexType>
    </xsd:element>
    <xsd:element name="Hyp">
      <xsd:complexType>
        <xsd:sequence>
          <xsd:group ref="termGroup"/>
        </xsd:sequence>
      </xsd:complexType>
    </xsd:element>
  </xsd:choice>
</xsd:group>

</xsd:schema>