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