# HG changeset patch
# User urbanc
# Date 1298224074 0
# Node ID 6b4c20714b4f6ab7dc4cb3f45b323fb887b66046
# Parent  3e4ad22193e7dda6684c0c1d807c2b581885afcb
chunhan's comments

diff -r 3e4ad22193e7 -r 6b4c20714b4f Paper/Paper.thy
--- a/Paper/Paper.thy	Sun Feb 20 13:43:00 2011 +0000
+++ b/Paper/Paper.thy	Sun Feb 20 17:47:54 2011 +0000
@@ -921,7 +921,7 @@
 
   \noindent
   It states that if an image of a set under an injective function @{text f} (injective over this set) 
-  is finite, then @{text A} itself must be finite. We can use it to establish the following 
+  is finite, then the set @{text A} itself must be finite. We can use it to establish the following 
   two lemmas.
 
   \begin{lemma}\label{finone}
@@ -1157,7 +1157,7 @@
   
   \noindent
   The case for @{const STAR} is similar as @{const SEQ}, but poses a few extra challenges. When
-  we analyse the case that @{text "x @ z"} is element in @{text "A\<star>"} and @{text x} is not the 
+  we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the 
   empty string, we 
   have the following picture: