<!ELEMENT IsaExport (IsaTheory*)>

<!ELEMENT IsaTheory (Import*,Axiom*,Theorem*,Const*,RecDatatypes*,Function*,ClassDef*,Locale*)>

<!ATTLIST IsaTheory name CDATA #REQUIRED>

<!ELEMENT Import EMPTY>

<!ATTLIST Import name CDATA #REQUIRED>

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

<!ATTLIST Axiom name CDATA #REQUIRED>

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

<!ATTLIST Theorem name CDATA #REQUIRED>

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

<!ATTLIST Const name CDATA #REQUIRED>

<!ELEMENT RecDatatypes (Datatype*)>

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

<!ATTLIST Datatype name CDATA #REQUIRED>

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

<!ATTLIST Constructor name CDATA #REQUIRED>

<!ELEMENT Function ((TVar|TFree|Type),Equations*)>

<!ATTLIST Function name CDATA #REQUIRED>

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

<!ELEMENT ClassDef (Parent*,Assumption*,ClassParam*)>

<!ATTLIST ClassDef name CDATA #REQUIRED>

<!ELEMENT Parent EMPTY>

<!ATTLIST Parent name CDATA #REQUIRED>

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

<!ATTLIST Assumption name CDATA #REQUIRED>

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

<!ATTLIST ClassParam name CDATA #REQUIRED>

<!ELEMENT Locale (LocaleParam*,Assumption*,Theorem*,Parent*)>

<!ATTLIST Locale name CDATA #REQUIRED>

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

<!ATTLIST LocaleParam name CDATA #REQUIRED>

<!ATTLIST LocaleParam infix CDATA #IMPLIED>

<!ATTLIST LocaleParam infixl CDATA #IMPLIED>

<!ATTLIST LocaleParam infixr CDATA #IMPLIED>

<!ATTLIST LocaleParam mixfix_i CDATA #IMPLIED>

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

<!ATTLIST Const infix CDATA #IMPLIED>

<!ATTLIST Const infixl CDATA #IMPLIED>

<!ATTLIST Const infixr CDATA #IMPLIED>

<!ATTLIST Const mixfix_i CDATA #IMPLIED>

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

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