src/HOL/Lambda/ParRed.thy
changeset 1376 92f83b9d17e1
parent 1269 ee011b365770
child 1789 aade046ec6d5
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Thu Nov 30 12:58:44 1995 +0100
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Fri Dec 01 12:03:13 1995 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  consts  par_beta :: "(db * db) set"
     1.6  
     1.7 -syntax  "=>" :: "[db,db] => bool" (infixl 50)
     1.8 +syntax  "=>" :: [db,db] => bool (infixl 50)
     1.9  
    1.10  translations
    1.11    "s => t" == "(s,t) : par_beta"
    1.12 @@ -23,8 +23,8 @@
    1.13      beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
    1.14  
    1.15  consts
    1.16 -  cd  :: "db => db"
    1.17 -  deFun :: "db => db"
    1.18 +  cd  :: db => db
    1.19 +  deFun :: db => db
    1.20  
    1.21  primrec cd db
    1.22    cd_Var "cd(Var n) = Var n"