src/HOL/ex/MT.thy
changeset 12338 de0f4a63baa5
parent 5102 8c782c25a11e
child 15450 43dfc914d1b8
     1.1 --- a/src/HOL/ex/MT.thy	Sat Dec 01 18:51:46 2001 +0100
     1.2 +++ b/src/HOL/ex/MT.thy	Sat Dec 01 18:52:32 2001 +0100
     1.3 @@ -31,19 +31,19 @@
     1.4    TyEnv
     1.5  
     1.6  arities 
     1.7 -  Const :: term
     1.8 +  Const :: type
     1.9  
    1.10 -  ExVar :: term
    1.11 -  Ex :: term
    1.12 +  ExVar :: type
    1.13 +  Ex :: type
    1.14  
    1.15 -  TyConst :: term
    1.16 -  Ty :: term
    1.17 +  TyConst :: type
    1.18 +  Ty :: type
    1.19  
    1.20 -  Clos :: term
    1.21 -  Val :: term
    1.22 +  Clos :: type
    1.23 +  Val :: type
    1.24  
    1.25 -  ValEnv :: term
    1.26 -  TyEnv :: term
    1.27 +  ValEnv :: type
    1.28 +  TyEnv :: type
    1.29  
    1.30  consts
    1.31    c_app :: [Const, Const] => Const