src/Pure/Tools/isabelle.xsd
author wenzelm
Sat Mar 20 17:33:11 2010 +0100 (2010-03-20)
changeset 35845 e5980f0ad025
parent 23832 09ee9527ffce
permissions -rw-r--r--
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
berghofe@20658
     1
<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">
berghofe@20658
     2
berghofe@20658
     3
<xsd:element name="class">
berghofe@20658
     4
  <xsd:complexType>
berghofe@20658
     5
    <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
     6
  </xsd:complexType>
berghofe@20658
     7
</xsd:element>
berghofe@20658
     8
berghofe@20658
     9
<xsd:element name="type">
berghofe@20658
    10
  <xsd:complexType>
berghofe@20658
    11
    <xsd:group ref="typeGroup"/>
berghofe@20658
    12
  </xsd:complexType>
berghofe@20658
    13
</xsd:element>
berghofe@20658
    14
berghofe@20658
    15
<xsd:element name="types">
berghofe@20658
    16
  <xsd:complexType>
berghofe@20658
    17
    <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
berghofe@20658
    18
  </xsd:complexType>
berghofe@20658
    19
</xsd:element>
berghofe@20658
    20
berghofe@20658
    21
<xsd:group name="typeGroup">
berghofe@20658
    22
  <xsd:choice>
berghofe@20658
    23
    <xsd:element name="TVar">
berghofe@20658
    24
      <xsd:complexType>
berghofe@20658
    25
        <xsd:sequence>
berghofe@20658
    26
          <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
berghofe@20658
    27
        </xsd:sequence>
berghofe@20658
    28
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
    29
        <xsd:attribute name="index" type="xsd:integer"/>
berghofe@20658
    30
      </xsd:complexType>
berghofe@20658
    31
    </xsd:element>
berghofe@20658
    32
    <xsd:element name="TFree">
berghofe@20658
    33
      <xsd:complexType>
berghofe@20658
    34
        <xsd:sequence>
berghofe@20658
    35
          <xsd:element ref="class" minOccurs="0" maxOccurs="unbounded"/>
berghofe@20658
    36
        </xsd:sequence>
berghofe@20658
    37
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
    38
      </xsd:complexType>
berghofe@20658
    39
    </xsd:element>
berghofe@20658
    40
    <xsd:element name="Type">
berghofe@20658
    41
      <xsd:complexType>
berghofe@20658
    42
        <xsd:sequence>
berghofe@20658
    43
          <xsd:group ref="typeGroup" minOccurs="0" maxOccurs="unbounded"/>
berghofe@20658
    44
        </xsd:sequence>
berghofe@20658
    45
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
    46
      </xsd:complexType>
berghofe@20658
    47
    </xsd:element>
berghofe@20658
    48
  </xsd:choice>
berghofe@20658
    49
</xsd:group>
berghofe@20658
    50
berghofe@20658
    51
<xsd:element name="term">
berghofe@20658
    52
  <xsd:complexType>
berghofe@20658
    53
    <xsd:group ref="termGroup"/>
berghofe@20658
    54
  </xsd:complexType>
berghofe@20658
    55
</xsd:element>
berghofe@20658
    56
berghofe@20658
    57
<xsd:group name="termGroup">
berghofe@20658
    58
  <xsd:choice>
berghofe@20658
    59
    <xsd:element name="Var">
berghofe@20658
    60
      <xsd:complexType>
berghofe@20658
    61
        <xsd:sequence>
berghofe@20658
    62
          <xsd:group ref="typeGroup"/>
berghofe@20658
    63
        </xsd:sequence>
berghofe@20658
    64
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
    65
        <xsd:attribute name="index" type="xsd:integer"/>
berghofe@20658
    66
      </xsd:complexType>
berghofe@20658
    67
    </xsd:element>
berghofe@20658
    68
    <xsd:element name="Free">
berghofe@20658
    69
      <xsd:complexType>
berghofe@20658
    70
        <xsd:sequence>
berghofe@20658
    71
          <xsd:group ref="typeGroup"/>
berghofe@20658
    72
        </xsd:sequence>
berghofe@20658
    73
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
    74
      </xsd:complexType>
berghofe@20658
    75
    </xsd:element>
berghofe@20658
    76
    <xsd:element name="Const">
berghofe@20658
    77
      <xsd:complexType>
berghofe@20658
    78
        <xsd:sequence>
berghofe@20658
    79
          <xsd:group ref="typeGroup"/>
berghofe@20658
    80
        </xsd:sequence>
berghofe@20658
    81
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
    82
      </xsd:complexType>
berghofe@20658
    83
    </xsd:element>
berghofe@20658
    84
    <xsd:element name="Bound">
berghofe@20658
    85
      <xsd:complexType>
berghofe@20658
    86
        <xsd:attribute name="index" type="xsd:integer" use="required"/>
berghofe@20658
    87
      </xsd:complexType>
berghofe@20658
    88
    </xsd:element>
berghofe@20658
    89
    <xsd:element name="App">
berghofe@20658
    90
      <xsd:complexType>
berghofe@20658
    91
        <xsd:sequence>
berghofe@20658
    92
          <xsd:group ref="termGroup"/>
berghofe@20658
    93
          <xsd:group ref="termGroup"/>
berghofe@20658
    94
        </xsd:sequence>
berghofe@20658
    95
      </xsd:complexType>
berghofe@20658
    96
    </xsd:element>
berghofe@20658
    97
    <xsd:element name="Abs">
berghofe@20658
    98
      <xsd:complexType>
berghofe@20658
    99
        <xsd:sequence>
berghofe@20658
   100
          <xsd:group ref="typeGroup"/>
berghofe@20658
   101
          <xsd:group ref="termGroup"/>
berghofe@20658
   102
        </xsd:sequence>
berghofe@20658
   103
        <xsd:attribute name="vname" type="xsd:string" use="required"/>
berghofe@20658
   104
      </xsd:complexType>
berghofe@20658
   105
    </xsd:element>
berghofe@20658
   106
  </xsd:choice>
berghofe@20658
   107
</xsd:group>
berghofe@20658
   108
berghofe@20658
   109
<xsd:element name="proof">
berghofe@20658
   110
  <xsd:complexType>
berghofe@20658
   111
    <xsd:group ref="proofGroup"/>
berghofe@20658
   112
  </xsd:complexType>
berghofe@20658
   113
</xsd:element>
berghofe@20658
   114
berghofe@20658
   115
<xsd:group name="proofGroup">
berghofe@20658
   116
  <xsd:choice>
berghofe@20658
   117
    <xsd:element name="PThm">
berghofe@20658
   118
      <xsd:complexType>
berghofe@20658
   119
        <xsd:sequence>
berghofe@20658
   120
          <xsd:group ref="termGroup" minOccurs="0"/>
berghofe@20658
   121
          <xsd:element ref="types" minOccurs="0"/>
berghofe@20658
   122
        </xsd:sequence>
berghofe@20658
   123
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
   124
      </xsd:complexType>
berghofe@20658
   125
    </xsd:element>
berghofe@20658
   126
    <xsd:element name="PAxm">
berghofe@20658
   127
      <xsd:complexType>
berghofe@20658
   128
        <xsd:sequence>
berghofe@20658
   129
          <xsd:group ref="termGroup" minOccurs="0"/>
berghofe@20658
   130
          <xsd:element ref="types" minOccurs="0"/>
berghofe@20658
   131
        </xsd:sequence>
berghofe@20658
   132
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
   133
      </xsd:complexType>
berghofe@20658
   134
    </xsd:element>
berghofe@20658
   135
    <xsd:element name="Oracle">
berghofe@20658
   136
      <xsd:complexType>
berghofe@20658
   137
        <xsd:sequence>
berghofe@20658
   138
          <xsd:group ref="termGroup"/>
berghofe@20658
   139
          <xsd:element ref="types" minOccurs="0"/>
berghofe@20658
   140
        </xsd:sequence>
berghofe@20658
   141
        <xsd:attribute name="name" type="xsd:string" use="required"/>
berghofe@20658
   142
      </xsd:complexType>
berghofe@20658
   143
    </xsd:element>
berghofe@20658
   144
    <xsd:element name="PBound">
berghofe@20658
   145
      <xsd:complexType>
berghofe@20658
   146
        <xsd:attribute name="index" type="xsd:integer" use="required"/>
berghofe@20658
   147
      </xsd:complexType>
berghofe@20658
   148
    </xsd:element>
berghofe@20658
   149
    <xsd:element name="Appt">
berghofe@20658
   150
      <xsd:complexType>
berghofe@20658
   151
        <xsd:sequence>
berghofe@20658
   152
          <xsd:group ref="proofGroup"/>
berghofe@20658
   153
          <xsd:group ref="termGroup" minOccurs="0"/>
berghofe@20658
   154
        </xsd:sequence>
berghofe@20658
   155
      </xsd:complexType>
berghofe@20658
   156
    </xsd:element>
berghofe@20658
   157
    <xsd:element name="AppP">
berghofe@20658
   158
      <xsd:complexType>
berghofe@20658
   159
        <xsd:sequence>
berghofe@20658
   160
          <xsd:group ref="proofGroup"/>
berghofe@20658
   161
          <xsd:group ref="proofGroup"/>
berghofe@20658
   162
        </xsd:sequence>
berghofe@20658
   163
      </xsd:complexType>
berghofe@20658
   164
    </xsd:element>
berghofe@20658
   165
    <xsd:element name="Abst">
berghofe@20658
   166
      <xsd:complexType>
berghofe@20658
   167
        <xsd:sequence>
berghofe@20658
   168
          <xsd:group ref="typeGroup" minOccurs="0"/>
berghofe@20658
   169
          <xsd:group ref="proofGroup"/>
berghofe@20658
   170
        </xsd:sequence>
berghofe@20658
   171
        <xsd:attribute name="vname" type="xsd:string" use="required"/>
berghofe@20658
   172
      </xsd:complexType>
berghofe@20658
   173
    </xsd:element>
berghofe@20658
   174
    <xsd:element name="AbsP">
berghofe@20658
   175
      <xsd:complexType>
berghofe@20658
   176
        <xsd:sequence>
berghofe@20658
   177
          <xsd:group ref="termGroup" minOccurs="0"/>
berghofe@20658
   178
          <xsd:group ref="proofGroup"/>
berghofe@20658
   179
        </xsd:sequence>
berghofe@20658
   180
        <xsd:attribute name="vname" type="xsd:string" use="required"/>
berghofe@20658
   181
      </xsd:complexType>
berghofe@20658
   182
    </xsd:element>
berghofe@23832
   183
    <xsd:element name="Hyp">
berghofe@23832
   184
      <xsd:complexType>
berghofe@23832
   185
        <xsd:sequence>
berghofe@23832
   186
          <xsd:group ref="termGroup"/>
berghofe@23832
   187
        </xsd:sequence>
berghofe@23832
   188
      </xsd:complexType>
berghofe@23832
   189
    </xsd:element>
berghofe@20658
   190
  </xsd:choice>
berghofe@20658
   191
</xsd:group>
berghofe@20658
   192
berghofe@20658
   193
</xsd:schema>