--- a/src/HOL/Lambda/Eta.thy Mon Sep 04 10:26:34 2000 +0200
+++ b/src/HOL/Lambda/Eta.thy Mon Sep 04 11:21:24 2000 +0200
@@ -26,9 +26,9 @@
"_eta_rtrancl" :: "[dB, dB] => bool" (infixl "-e>>" 50)
"_eta_reflcl" :: "[dB, dB] => bool" (infixl "-e>=" 50)
translations
- "s -e> t" == "(s,t) \<in> eta"
- "s -e>> t" == "(s,t) \<in> eta^*"
- "s -e>= t" == "(s,t) \<in> eta^="
+ "s -e> t" == "(s, t) \<in> eta"
+ "s -e>> t" == "(s, t) \<in> eta^*"
+ "s -e>= t" == "(s, t) \<in> eta^="
inductive eta
intros [simp, intro]