changeset 12338 | de0f4a63baa5 |
parent 5102 | 8c782c25a11e |
child 15450 | 43dfc914d1b8 |
--- a/src/HOL/ex/MT.thy Sat Dec 01 18:51:46 2001 +0100 +++ b/src/HOL/ex/MT.thy Sat Dec 01 18:52:32 2001 +0100 @@ -31,19 +31,19 @@ TyEnv arities - Const :: term + Const :: type - ExVar :: term - Ex :: term + ExVar :: type + Ex :: type - TyConst :: term - Ty :: term + TyConst :: type + Ty :: type - Clos :: term - Val :: term + Clos :: type + Val :: type - ValEnv :: term - TyEnv :: term + ValEnv :: type + TyEnv :: type consts c_app :: [Const, Const] => Const