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

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

<!ATTLIST Locale name CDATA #REQUIRED>

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

<!ATTLIST Cls name CDATA #REQUIRED>

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

<!ATTLIST TypeSynonym name CDATA #REQUIRED>

<!ATTLIST TypeSynonym mixfix CDATA #IMPLIED>

<!ATTLIST TypeSynonym target CDATA #IMPLIED>

<!ELEMENT Datatypes (Datatype+)>

<!ELEMENT Datatype (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 (Const+)>

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

<!ATTLIST Const name CDATA #REQUIRED>

<!ATTLIST Const 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 ((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 (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 (FunSig+,(Bound|Free|Var|Const|App|Abs)+)>

<!ATTLIST Primrec target CDATA #IMPLIED>

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