src/HOL/Nominal/Examples/VC_Condition.thy

--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Tue Jan 08 11:37:37 2008 +0100
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Tue Jan 08 23:11:08 2008 +0100
@@ -90,7 +90,7 @@
 
 text {*
   The next lemma shows by induction on xs that if x is a free 
-  variable in t and x does not occur in xs, then x is a free 
+  variable in t, and x does not occur in xs, then x is a free 
   variable in bind xs t. In the nominal tradition we formulate    
   'is a free variable in' as 'is not fresh for'. *}
 lemma free_variable: