src/HOL/Lambda/Eta.thy
changeset 1376 92f83b9d17e1
parent 1269 ee011b365770
child 1789 aade046ec6d5
     1.1 --- a/src/HOL/Lambda/Eta.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/Lambda/Eta.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -7,11 +7,11 @@
     1.4  *)
     1.5  
     1.6  Eta = ParRed + Commutation +
     1.7 -consts free :: "db => nat => bool"
     1.8 -       decr :: "[db,nat] => db"
     1.9 +consts free :: db => nat => bool
    1.10 +       decr :: [db,nat] => db
    1.11         eta  :: "(db * db) set"
    1.12  
    1.13 -syntax  "-e>", "-e>>", "-e>=" , "->=" :: "[db,db] => bool" (infixl 50)
    1.14 +syntax  "-e>", "-e>>", "-e>=" , "->=" :: [db,db] => bool (infixl 50)
    1.15  
    1.16  translations
    1.17    "s -e>  t" == "(s,t) : eta"