diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Lambda/Lambda.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -57,13 +57,15 @@
   beta :: "(dB \<times> dB) set"
 
 abbreviation
-  beta_red :: "[dB, dB] => bool"  (infixl "->" 50)
+  beta_red :: "[dB, dB] => bool"  (infixl "->" 50) where
   "s -> t == (s, t) \<in> beta"
-  beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50)
+
+abbreviation
+  beta_reds :: "[dB, dB] => bool"  (infixl "->>" 50) where
   "s ->> t == (s, t) \<in> beta^*"
 
 notation (latex)
-  beta_red  (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+  beta_red  (infixl "\<rightarrow>\<^sub>\<beta>" 50) and
   beta_reds  (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
 
 inductive beta