--- a/src/HOL/Lambda/Eta.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Lambda/Eta.thy Fri Nov 17 02:20:03 2006 +0100
@@ -22,11 +22,15 @@
eta :: "(dB \<times> dB) set"
abbreviation
- eta_red :: "[dB, dB] => bool" (infixl "-e>" 50)
+ eta_red :: "[dB, dB] => bool" (infixl "-e>" 50) where
"s -e> t == (s, t) \<in> eta"
- eta_reds :: "[dB, dB] => bool" (infixl "-e>>" 50)
+
+abbreviation
+ eta_reds :: "[dB, dB] => bool" (infixl "-e>>" 50) where
"s -e>> t == (s, t) \<in> eta^*"
- eta_red0 :: "[dB, dB] => bool" (infixl "-e>=" 50)
+
+abbreviation
+ eta_red0 :: "[dB, dB] => bool" (infixl "-e>=" 50) where
"s -e>= t == (s, t) \<in> eta^="
inductive eta
@@ -224,7 +228,7 @@
par_eta :: "(dB \<times> dB) set"
abbreviation
- par_eta_red :: "[dB, dB] => bool" (infixl "=e>" 50)
+ par_eta_red :: "[dB, dB] => bool" (infixl "=e>" 50) where
"s =e> t == (s, t) \<in> par_eta"
notation (xsymbols)