changeset 251 | 821ff177a478 |
parent 250 | b1946e131ce8 |
child 252 | 8e2c497d699e |
--- a/Journal/Paper.thy Tue Sep 13 12:00:53 2011 +0000 +++ b/Journal/Paper.thy Wed Sep 14 11:46:50 2011 +0000 @@ -2205,7 +2205,7 @@ \noindent and use \eqref{supseqprops} to establish that @{thm lang_UP} holds. This shows - that @{term "SUBSEQ A"} is regular, provided @{text A} is. + that @{term "SUPSEQ A"} is regular, provided @{text A} is. \end{proof} \noindent