diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/Paper/document/root.tex
--- a/thys/Paper/document/root.tex	Sun May 08 09:49:21 2016 +0100
+++ b/thys/Paper/document/root.tex	Mon May 09 12:09:56 2016 +0100
@@ -68,8 +68,7 @@
 algorithm. Our definitions and proof are much simpler than those by
 Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the
 second part we analyse the correctness argument by Sulzmann and Lu and
-explain why it seems hard to turn it into a proof rigorous enough to
-be accepted by a system such as Isabelle/HOL.\smallskip
+explain why the gaps in this argument cannot be filled easily.\smallskip
 
 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,
 Isabelle/HOL