src/HOL/Lambda/Eta.thy
changeset 9827 ce6e22ff89c3
parent 9811 39ffdb8cab03
child 9858 c3ac6128b649
--- 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]