src/HOL/Lambda/Lambda.thy
changeset 1376 92f83b9d17e1
parent 1269 ee011b365770
child 1789 aade046ec6d5
     1.1 --- a/src/HOL/Lambda/Lambda.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/Lambda/Lambda.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -12,11 +12,11 @@
     1.4  datatype db = Var nat | "@" db db (infixl 200) | Fun db
     1.5  
     1.6  consts
     1.7 -  subst  :: "[db,db,nat]=>db" ("_[_'/_]" [300,0,0] 300)
     1.8 -  lift   :: "[db,nat] => db"
     1.9 +  subst  :: [db,db,nat]=>db ("_[_'/_]" [300,0,0] 300)
    1.10 +  lift   :: [db,nat] => db
    1.11    (* optimized versions *)
    1.12 -  substn :: "[db,db,nat] => db"
    1.13 -  liftn  :: "[nat,db,nat] => db"
    1.14 +  substn :: [db,db,nat] => db
    1.15 +  liftn  :: [nat,db,nat] => db
    1.16  
    1.17  primrec lift db
    1.18    lift_Var "lift (Var i) k = (if i < k then Var i else Var(Suc i))"
    1.19 @@ -42,7 +42,7 @@
    1.20  
    1.21  consts  beta :: "(db * db) set"
    1.22  
    1.23 -syntax  "->", "->>" :: "[db,db] => bool" (infixl 50)
    1.24 +syntax  "->", "->>" :: [db,db] => bool (infixl 50)
    1.25  
    1.26  translations
    1.27    "s -> t"  == "(s,t) : beta"