
diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Lambda/ParRed.thy
--- a/src/HOL/Lambda/ParRed.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Lambda/ParRed.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -18,7 +18,7 @@
   par_beta :: "(dB \<times> dB) set"
 
 abbreviation
-  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50)
+  par_beta_red :: "[dB, dB] => bool"  (infixl "=>" 50) where
   "s => t == (s, t) \<in> par_beta"
 
 inductive par_beta




