<!ELEMENT Export (Thy+)>

<!ELEMENT Thy (Import+,Keyword*,UseFile*,Body)>

<!ATTLIST Thy name CDATA #REQUIRED>

<!ATTLIST Thy header CDATA #IMPLIED>

<!-- Header -->

<!ELEMENT Keyword EMPTY>

<!ATTLIST Keyword name CDATA #REQUIRED>

<!ELEMENT Import EMPTY>

<!ATTLIST Import name CDATA #REQUIRED>

<!ELEMENT UseFile EMPTY>

<!ATTLIST UseFile name CDATA #REQUIRED>

<!-- Body -->

<!ELEMENT Body (Locale|Cls|TypeSynonym|Datatypes|Consts|Axioms|Lemma|Definition|Fun|Instantiation|Instance|Subclass)*>

<!ELEMENT Locale (Ctxt,SigData,Parent*,Body)>

<!ATTLIST Locale name CDATA #REQUIRED>

<!ELEMENT Cls (Ctxt,SigData,Parent*,Body)>

<!ATTLIST Cls name CDATA #REQUIRED>

<!ELEMENT TypeSynonym (SigData,Vars,(TVar|TFree|Type))>

<!ATTLIST TypeSynonym name CDATA #REQUIRED>

<!ATTLIST TypeSynonym mixfix CDATA #IMPLIED>

<!ATTLIST TypeSynonym target CDATA #IMPLIED>

<!ELEMENT Datatypes (Datatype+)>

<!ELEMENT Datatype (SigData,Constructor+,TFree*)>

<!ATTLIST Datatype name CDATA #REQUIRED>

<!ATTLIST Datatype mixfix CDATA #REQUIRED>

<!ELEMENT Constructor ((TVar|TFree|Type)*)>

<!ATTLIST Constructor name CDATA #REQUIRED>

<!ATTLIST Constructor mixfix CDATA #IMPLIED>

<!ELEMENT Consts (ConstDef+)>

<!ELEMENT ConstDef (SigData,(TVar|TFree|Type))>

<!ATTLIST ConstDef name CDATA #REQUIRED>

<!ATTLIST ConstDef mixfix CDATA #IMPLIED>

<!ELEMENT Axioms (Axiom)+>

<!ELEMENT Axiom ((Bound|Free|Var|Const|App|Abs))>

<!ATTLIST Axiom name CDATA #REQUIRED>

<!ATTLIST Axiom args CDATA #REQUIRED>

<!ELEMENT Lemma (Ctxt,Proof,(Shows)+)>

<!ATTLIST Lemma target CDATA #IMPLIED>

<!ELEMENT Definition (SigData,(TVar|TFree|Type)?,(Bound|Free|Var|Const|App|Abs))>

<!ATTLIST Definition name CDATA #IMPLIED>

<!ATTLIST Definition target CDATA #IMPLIED>

<!ATTLIST Definition mixfix CDATA #IMPLIED>

<!ELEMENT Fun (SigData,FunSig+,(Bound|Free|Var|Const|App|Abs)+)>

<!ATTLIST Fun target CDATA #IMPLIED>

<!ATTLIST Fun sequential CDATA #IMPLIED>

<!ATTLIST Fun default CDATA #IMPLIED>

<!ATTLIST Fun domintros CDATA #IMPLIED>

<!ATTLIST Fun partials CDATA #IMPLIED>

<!ELEMENT FunSig (TVar|TFree|Type)?>

<!ATTLIST FunSig name CDATA #REQUIRED>

<!ATTLIST FunSig mixfix CDATA #IMPLIED>

<!ELEMENT Primrec (SigData,FunSig+,(Bound|Free|Var|Const|App|Abs)+)>

<!ATTLIST Primrec target CDATA #IMPLIED>

<!ELEMENT Instantiation (Arity,Body)>

<!ATTLIST Instantiation type CDATA #REQUIRED>

<!ELEMENT Instance (Proof,(Vars,Arity)?)>

<!ATTLIST Instance class CDATA #IMPLIED>

<!ATTLIST Instance rel CDATA #IMPLIED>

<!ATTLIST Instance class1 CDATA #IMPLIED>

<!ELEMENT Subclass (Proof)>

<!ATTLIST Subclass class CDATA #REQUIRED>

<!ELEMENT Sort (class+)>

<!ELEMENT Arity (Sort,Sort*)>

<!ELEMENT Vars (TFree*)>

<!ELEMENT Parent EMPTY>

<!ATTLIST Parent name CDATA #REQUIRED>

<!ELEMENT Fixes (Fix*)>

<!ELEMENT Fix ((TVar|TFree|Type)?)>

<!ATTLIST Fix name CDATA #REQUIRED>

<!ATTLIST Fix mixfix CDATA #IMPLIED>

<!ELEMENT Assumes (Assumption*)>

<!ELEMENT Assumption ((Bound|Free|Var|Const|App|Abs))>

<!ATTLIST Assumption name CDATA #REQUIRED>

<!ATTLIST Assumption args CDATA #REQUIRED>

<!ELEMENT Ctxt (Fixes?,Assumes?)>

<!ELEMENT SigData (AddType|AddConst|AddTypeSynonym)*>

<!ELEMENT AddConst ((TVar|TFree|Type)?,(Arg|String|Break|Block)*)>

<!ATTLIST AddConst name CDATA #REQUIRED>

<!ATTLIST AddConst nargs CDATA #IMPLIED>

<!ATTLIST AddConst prio CDATA #IMPLIED>

<!ELEMENT Arg EMPTY>

<!ATTLIST Arg prio CDATA #REQUIRED>

<!ELEMENT String EMPTY>

<!ATTLIST String val CDATA #REQUIRED>

<!ELEMENT Break EMPTY>

<!ATTLIST Break prio CDATA #REQUIRED>

<!ELEMENT Block ((Arg|String|Break|Block)*)>

<!ATTLIST Block prio CDATA #REQUIRED>

<!ELEMENT AddType ((Arg|String|Break|Block)*)>

<!ATTLIST AddType name CDATA #REQUIRED>

<!ATTLIST AddType arity CDATA #REQUIRED>

<!ATTLIST AddType nargs CDATA #IMPLIED>

<!ATTLIST AddType prio CDATA #IMPLIED>

<!ELEMENT AddTypeSynonym ((TVar|TFree|Type))>

<!ATTLIST AddTypeSynonym name CDATA #REQUIRED>

<!ELEMENT Proof (#PCDATA)>

<!ELEMENT Shows (Show+)>

<!ATTLIST Shows name CDATA #REQUIRED>

<!ATTLIST Shows args CDATA #REQUIRED>

<!ELEMENT Show ((Bound|Free|Var|Const|App|Abs)+)>

<!-- Term -->

<!ELEMENT Bound EMPTY>

<!ATTLIST Bound index CDATA #REQUIRED>

<!ELEMENT Free (TVar|TFree|Type)>

<!ATTLIST Free name CDATA #REQUIRED>

<!ELEMENT Var (TVar|TFree|Type)>

<!ATTLIST Var name CDATA #REQUIRED>

<!ATTLIST Var index CDATA #IMPLIED>

<!ELEMENT Const ((TVar|TFree|Type))>

<!ATTLIST Const name CDATA #REQUIRED>

<!ELEMENT App ((Bound|Free|Var|Const|App|Abs), (Bound|Free|Var|Const|App|Abs))>

<!ELEMENT Abs ((TVar|TFree|Type), (Bound|Free|Var|Const|App|Abs))>

<!ATTLIST Abs vname CDATA #REQUIRED>

<!-- Type -->

<!ELEMENT TVar (Class*)>

<!ATTLIST TVar name CDATA #REQUIRED>

<!ATTLIST TVar index CDATA #IMPLIED>

<!ELEMENT TFree (Class*)>

<!ATTLIST TFree name CDATA #REQUIRED>

<!ELEMENT Type ((TVar|TFree|Type)*)>

<!ATTLIST Type name CDATA #REQUIRED>

<!ELEMENT class EMPTY>

<!ATTLIST class name CDATA #REQUIRED>