src/HOL/Lambda/ParRed.thy

 
 ParRed = Lambda + Commutation +
 
 consts  par_beta :: "(db * db) set"
 
-syntax  "=>" :: "[db,db] => bool" (infixl 50)
+syntax  "=>" :: [db,db] => bool (infixl 50)
 
 translations
   "s => t" == "(s,t) : par_beta"
 
 inductive "par_beta"

     abs   "s => t ==> Fun s => Fun t"
     app   "[| s => s'; t => t' |] ==> s @ t => s' @ t'"
     beta  "[| s => s'; t => t' |] ==> (Fun s) @ t => s'[t'/0]"
 
 consts
-  cd  :: "db => db"
-  deFun :: "db => db"
+  cd  :: db => db
+  deFun :: db => db
 
 primrec cd db
   cd_Var "cd(Var n) = Var n"
   cd_App "cd(s @ t) = (case s of
             Var n => s @ (cd t) |