<!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|Domains|Consts|Axioms|Lemma|Definition|Funs|Primrec|Fixrec|Instantiation|Instance|Subclass|Typedef|Defs)*>

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

<!ATTLIST Locale name CDATA #REQUIRED>

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

<!ATTLIST Cls name CDATA #REQUIRED>

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

<!ATTLIST TypeSynonym name CDATA #REQUIRED>

<!ATTLIST TypeSynonym target CDATA #IMPLIED>

<!ELEMENT Datatypes (Datatype+)>

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

<!ATTLIST Datatype name CDATA #REQUIRED>

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

<!ATTLIST Constructor name CDATA #IMPLIED>

<!ELEMENT Domains (Domain+)>

<!ELEMENT Domain (Mixfix?,TFree*,DomainConstructor+)>

<!ATTLIST Domain name CDATA #REQUIRED>

<!ELEMENT DomainConstructor ((TVar|TFree|Type),DomainConstructorArg*)>

<!ATTLIST DomainConstructor name CDATA #REQUIRED>

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

<!ATTLIST DomainConstructorArg lazy CDATA #IMPLIED>

<!ATTLIST DomainConstructorArg name CDATA #IMPLIED>

<!ELEMENT Consts (ConstDef+)>

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

<!ATTLIST ConstDef name CDATA #REQUIRED>

<!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 (Mixfix?,(TVar|TFree|Type),(Bound|Free|Var|Const|App|Abs)+)>

<!ATTLIST Definition name CDATA #REQUIRED>

<!ATTLIST Definition target CDATA #IMPLIED>

<!ELEMENT Funs (Fun+)>

<!ATTLIST Funs target CDATA #IMPLIED>

<!ATTLIST Funs sequential CDATA #IMPLIED>

<!ATTLIST Funs default CDATA #IMPLIED>

<!ATTLIST Funs domintros CDATA #IMPLIED>

<!ATTLIST Funs partials CDATA #IMPLIED>

<!ELEMENT Fun (Mixfix?,(TVar|TFree|Type),Equation+)>

<!ATTLIST Fun name CDATA #REQUIRED>

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

<!ELEMENT Primrec (Fun+)>

<!ATTLIST Primrec target CDATA #IMPLIED>

<!ELEMENT Fixrec (FixrecFun+)>

<!ELEMENT FixrecFun (Mixfix?,(TVar|TFree|Type),FixrecEquation+)>

<!ATTLIST FixrecFun name CDATA #REQUIRED>

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

<!ATTLIST FixrecEquation unchecked CDATA #IMPLIED>

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

<!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>

<!ATTLIST Subclass target CDATA #IMPLIED>

<!ELEMENT Typedef (Mixfix?,Proof,(Bound|Free|Var|Const|App|Abs),TFree*)>

<!ATTLIST Typedef type CDATA #REQUIRED>

<!ATTLIST Typedef m1 CDATA #IMPLIED>

<!ATTLIST Typedef m2 CDATA #IMPLIED>

<!ELEMENT Defs (Def+)>

<!ATTLIST Defs unchecked CDATA #IMPLIED>

<!ATTLIST Defs overloaded CDATA #IMPLIED>

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

<!ATTLIST Def name CDATA #REQUIRED>

<!ATTLIST Def args CDATA #REQUIRED>

<!ATTLIST Def const 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),Mixfix?)>

<!ATTLIST Fix name CDATA #REQUIRED>

<!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 Mixfix ((Arg|String|Break|Block)*)>

<!ATTLIST Mixfix nargs CDATA #REQUIRED>

<!ATTLIST Mixfix prio CDATA #REQUIRED>

<!ATTLIST Mixfix pretty CDATA #REQUIRED>

<!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 Proof (#PCDATA)>

<!ELEMENT Shows (Show+)>

<!ATTLIST Shows name CDATA #REQUIRED>

<!ATTLIST Shows args CDATA #IMPLIED>

<!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>