--- a/src/HOL/Lambda/Lambda.thy Thu Feb 16 21:11:58 2006 +0100
+++ b/src/HOL/Lambda/Lambda.thy Thu Feb 16 21:12:00 2006 +0100
@@ -56,15 +56,15 @@
consts
beta :: "(dB \<times> dB) set"
-syntax
- "_beta" :: "[dB, dB] => bool" (infixl "->" 50)
- "_beta_rtrancl" :: "[dB, dB] => bool" (infixl "->>" 50)
+abbreviation (output)
+ beta_red :: "[dB, dB] => bool" (infixl "->" 50)
+ "(s -> t) = ((s, t) \<in> beta)"
+ beta_reds :: "[dB, dB] => bool" (infixl "->>" 50)
+ "(s ->> t) = ((s, t) \<in> beta^*)"
+
syntax (latex)
- "_beta" :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
- "_beta_rtrancl" :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
-translations
- "s \<rightarrow>\<^sub>\<beta> t" == "(s, t) \<in> beta"
- "s \<rightarrow>\<^sub>\<beta>\<^sup>* t" == "(s, t) \<in> beta^*"
+ beta_red :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>" 50)
+ beta_reds :: "[dB, dB] => bool" (infixl "\<rightarrow>\<^sub>\<beta>\<^sup>*" 50)
inductive beta
intros