src/HOL/Lambda/ParRed.thy
changeset 21404 eb85850d3eb7
parent 20503 503ac4c5ef91
child 22271 51a80e238b29
     1.1 --- a/src/HOL/Lambda/ParRed.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Lambda/ParRed.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    par_beta :: "(dB \<times> dB) set"
     1.5  
     1.6  abbreviation
     1.7 -  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
     1.8 +  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50) where
     1.9    "s => t == (s, t) \<in> par_beta"
    1.10  
    1.11  inductive par_beta