src/HOL/ex/MT.thy
changeset 12338 de0f4a63baa5
parent 5102 8c782c25a11e
child 15450 43dfc914d1b8
equal deleted inserted replaced
12337:7c6a970f0808 12338:de0f4a63baa5
    29 
    29 
    30   ValEnv
    30   ValEnv
    31   TyEnv
    31   TyEnv
    32 
    32 
    33 arities 
    33 arities 
    34   Const :: term
    34   Const :: type
    35 
    35 
    36   ExVar :: term
    36   ExVar :: type
    37   Ex :: term
    37   Ex :: type
    38 
    38 
    39   TyConst :: term
    39   TyConst :: type
    40   Ty :: term
    40   Ty :: type
    41 
    41 
    42   Clos :: term
    42   Clos :: type
    43   Val :: term
    43   Val :: type
    44 
    44 
    45   ValEnv :: term
    45   ValEnv :: type
    46   TyEnv :: term
    46   TyEnv :: type
    47 
    47 
    48 consts
    48 consts
    49   c_app :: [Const, Const] => Const
    49   c_app :: [Const, Const] => Const
    50 
    50 
    51   e_const :: Const => Ex
    51   e_const :: Const => Ex