src/HOL/ex/MT.thy
changeset 1376 92f83b9d17e1
parent 1151 c820b3cc3df0
child 1476 608483c2122a
     1.1 --- a/src/HOL/ex/MT.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/ex/MT.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -46,48 +46,48 @@
     1.4    TyEnv :: term
     1.5  
     1.6  consts
     1.7 -  c_app :: "[Const, Const] => Const"
     1.8 +  c_app :: [Const, Const] => Const
     1.9  
    1.10 -  e_const :: "Const => Ex"
    1.11 -  e_var :: "ExVar => Ex"
    1.12 -  e_fn :: "[ExVar, Ex] => Ex" ("fn _ => _" [0,51] 1000)
    1.13 -  e_fix :: "[ExVar, ExVar, Ex] => Ex" ("fix _ ( _ ) = _" [0,51,51] 1000)
    1.14 -  e_app :: "[Ex, Ex] => Ex" ("_ @ _" [51,51] 1000)
    1.15 -  e_const_fst :: "Ex => Const"
    1.16 +  e_const :: Const => Ex
    1.17 +  e_var :: ExVar => Ex
    1.18 +  e_fn :: [ExVar, Ex] => Ex ("fn _ => _" [0,51] 1000)
    1.19 +  e_fix :: [ExVar, ExVar, Ex] => Ex ("fix _ ( _ ) = _" [0,51,51] 1000)
    1.20 +  e_app :: [Ex, Ex] => Ex ("_ @ _" [51,51] 1000)
    1.21 +  e_const_fst :: Ex => Const
    1.22  
    1.23 -  t_const :: "TyConst => Ty"
    1.24 -  t_fun :: "[Ty, Ty] => Ty" ("_ -> _" [51,51] 1000)
    1.25 +  t_const :: TyConst => Ty
    1.26 +  t_fun :: [Ty, Ty] => Ty ("_ -> _" [51,51] 1000)
    1.27  
    1.28 -  v_const :: "Const => Val"
    1.29 -  v_clos :: "Clos => Val"
    1.30 +  v_const :: Const => Val
    1.31 +  v_clos :: Clos => Val
    1.32    
    1.33 -  ve_emp :: "ValEnv"
    1.34 -  ve_owr :: "[ValEnv, ExVar, Val] => ValEnv" ("_ + { _ |-> _ }" [36,0,0] 50)
    1.35 -  ve_dom :: "ValEnv => ExVar set"
    1.36 -  ve_app :: "[ValEnv, ExVar] => Val"
    1.37 +  ve_emp :: ValEnv
    1.38 +  ve_owr :: [ValEnv, ExVar, Val] => ValEnv ("_ + { _ |-> _ }" [36,0,0] 50)
    1.39 +  ve_dom :: ValEnv => ExVar set
    1.40 +  ve_app :: [ValEnv, ExVar] => Val
    1.41  
    1.42 -  clos_mk :: "[ExVar, Ex, ValEnv] => Clos" ("<| _ , _ , _ |>" [0,0,0] 1000)
    1.43 +  clos_mk :: [ExVar, Ex, ValEnv] => Clos ("<| _ , _ , _ |>" [0,0,0] 1000)
    1.44  
    1.45 -  te_emp :: "TyEnv"
    1.46 -  te_owr :: "[TyEnv, ExVar, Ty] => TyEnv" ("_ + { _ |=> _ }" [36,0,0] 50)
    1.47 -  te_app :: "[TyEnv, ExVar] => Ty"
    1.48 -  te_dom :: "TyEnv => ExVar set"
    1.49 +  te_emp :: TyEnv
    1.50 +  te_owr :: [TyEnv, ExVar, Ty] => TyEnv ("_ + { _ |=> _ }" [36,0,0] 50)
    1.51 +  te_app :: [TyEnv, ExVar] => Ty
    1.52 +  te_dom :: TyEnv => ExVar set
    1.53  
    1.54    eval_fun :: "((ValEnv * Ex) * Val) set => ((ValEnv * Ex) * Val) set"
    1.55    eval_rel :: "((ValEnv * Ex) * Val) set"
    1.56 -  eval :: "[ValEnv, Ex, Val] => bool" ("_ |- _ ---> _" [36,0,36] 50)
    1.57 +  eval :: [ValEnv, Ex, Val] => bool ("_ |- _ ---> _" [36,0,36] 50)
    1.58  
    1.59    elab_fun :: "((TyEnv * Ex) * Ty) set => ((TyEnv * Ex) * Ty) set"
    1.60    elab_rel :: "((TyEnv * Ex) * Ty) set"
    1.61 -  elab :: "[TyEnv, Ex, Ty] => bool" ("_ |- _ ===> _" [36,0,36] 50)
    1.62 +  elab :: [TyEnv, Ex, Ty] => bool ("_ |- _ ===> _" [36,0,36] 50)
    1.63    
    1.64 -  isof :: "[Const, Ty] => bool" ("_ isof _" [36,36] 50)
    1.65 -  isof_env :: "[ValEnv,TyEnv] => bool" ("_ isofenv _")
    1.66 +  isof :: [Const, Ty] => bool ("_ isof _" [36,36] 50)
    1.67 +  isof_env :: [ValEnv,TyEnv] => bool ("_ isofenv _")
    1.68  
    1.69    hasty_fun :: "(Val * Ty) set => (Val * Ty) set"
    1.70    hasty_rel :: "(Val * Ty) set"
    1.71 -  hasty :: "[Val, Ty] => bool" ("_ hasty _" [36,36] 50)
    1.72 -  hasty_env :: "[ValEnv,TyEnv] => bool" ("_ hastyenv _ " [36,36] 35)
    1.73 +  hasty :: [Val, Ty] => bool ("_ hasty _" [36,36] 50)
    1.74 +  hasty_env :: [ValEnv,TyEnv] => bool ("_ hastyenv _ " [36,36] 35)
    1.75  
    1.76  rules
    1.77