src/HOL/Lambda/ListBeta.thy
changeset 9827 ce6e22ff89c3
parent 9811 39ffdb8cab03
child 9906 5c027cca6262
--- 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)"