--- 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]
--- a/src/HOL/Lambda/Lambda.thy Mon Sep 04 10:26:34 2000 +0200
+++ b/src/HOL/Lambda/Lambda.thy Mon Sep 04 11:21:24 2000 +0200
@@ -60,8 +60,8 @@
"_beta" :: "[dB, dB] => bool" (infixl "->" 50)
"_beta_rtrancl" :: "[dB, dB] => bool" (infixl "->>" 50)
translations
- "s -> t" == "(s,t) \<in> beta"
- "s ->> t" == "(s,t) \<in> beta^*"
+ "s -> t" == "(s, t) \<in> beta"
+ "s ->> t" == "(s, t) \<in> beta^*"
inductive beta
intros [simp, intro!]
--- a/src/HOL/Lambda/ListBeta.thy Mon Sep 04 10:26:34 2000 +0200
+++ b/src/HOL/Lambda/ListBeta.thy Mon Sep 04 11:21:24 2000 +0200
@@ -15,7 +15,7 @@
syntax
"_list_beta" :: "dB => dB => bool" (infixl "=>" 50)
translations
- "rs => ss" == "(rs,ss) : step1 beta"
+ "rs => ss" == "(rs, ss) : step1 beta"
lemma head_Var_reduction_aux:
"v -> v' ==> \<forall>rs. v = Var n $$ rs --> (\<exists>ss. rs => ss \<and> v' = Var n $$ ss)"