# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316599278 -7200
# Node ID 33a0b1a0e4b2d02a1497b2867d0226681a556ff9
# Parent  9133086a08173100bb80e9e55e1ab8645df0f78b
some polishing

diff -r 9133086a0817 -r 33a0b1a0e4b2 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 10:30:21 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 12:01:18 2011 +0200
@@ -1560,8 +1560,8 @@
   In this binding clause no atom is bound and we only have to `alpha-relate'
   the bodies. For this we build first the tuples @{text "D \<equiv> (d\<^isub>1,\<dots>,
   d\<^isub>q)"} and @{text "D' \<equiv> (d\<PRIME>\<^isub>1,\<dots>, d\<PRIME>\<^isub>q)"}
-  whereby the labels @{text "d"}$_{1..q}$ refer to the arguments @{text
-  "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to @{text
+  whereby the labels @{text "d"}$_{1..q}$ refer to some of the arguments @{text
+  "z"}$_{1..n}$ and respectively @{text "d\<PRIME>"}$_{1..q}$ to some of @{text
   "z\<PRIME>"}$_{1..n}$ of the term-constructor. In order to relate two such
   tuples we define the compound alpha-equivalence relation @{text "R"} as
   follows
@@ -1573,7 +1573,7 @@
   \noindent
   with @{text "R\<^isub>i"} being @{text "\<approx>ty\<^isub>i"} if the corresponding
   labels @{text "d\<^isub>i"} and @{text "d\<PRIME>\<^isub>i"} refer to a
-  recursive argument of @{text C} with type @{text "ty\<^isub>i"}; otherwise
+  recursive argument of @{text C} and have type @{text "ty\<^isub>i"}; otherwise
   we take @{text "R\<^isub>i"} to be the equality @{text "="}. Again the
   latter is because @{text "ty\<^isub>i"} is not part of the specified types
   and alpha-equivalence of any previously defined type is supposed to coincide