src/HOL/Lambda/ParRed.thy
changeset 1269 ee011b365770
parent 1126 50ac36140e21
child 1376 92f83b9d17e1
equal deleted inserted replaced
1268:f6ef556b3ede 1269:ee011b365770
     4     Copyright   1995 TU Muenchen
     4     Copyright   1995 TU Muenchen
     5 
     5 
     6 Parallel reduction and a complete developments function "cd".
     6 Parallel reduction and a complete developments function "cd".
     7 *)
     7 *)
     8 
     8 
     9 ParRed = Lambda + Confluence +
     9 ParRed = Lambda + Commutation +
    10 
    10 
    11 consts  par_beta :: "(db * db) set"
    11 consts  par_beta :: "(db * db) set"
    12 
    12 
    13 syntax  "=>" :: "[db,db] => bool" (infixl 50)
    13 syntax  "=>" :: "[db,db] => bool" (infixl 50)
    14 
    14