isabelle: src/Pure/Tools/isabelle.xsd@0ebcd575d3c6 (annotated)

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

author	paulson
	Fri, 05 Oct 2007 09:59:03 +0200
changeset 24854	0ebcd575d3c6
parent 23832	09ee9527ffce
permissions	-rw-r--r--