| 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)"