--- a/Journal/Paper.thy Wed Sep 14 21:14:50 2011 +0000
+++ b/Journal/Paper.thy Thu Sep 15 12:46:00 2011 +0000
@@ -2154,7 +2154,7 @@
is restricted to 2-letter alphabets,
which means also our formalisation of Theorem~\ref{subseqreg} is `tainted' with
this constraint. However our methodology is applicable to any alphabet of finite size.}
- Higman's Lemma allows us to infer that every set @{text A} of antichains, satisfying
+ Higman's Lemma allows us to infer that every language @{text A} of antichains, satisfying
\begin{equation}\label{higman}
@{text "\<forall>x, y \<in> A."}~@{term "x \<noteq> y \<longrightarrow> \<not>(x \<preceq> y) \<and> \<not>(y \<preceq> x)"}