--- a/thys/Paper/Paper.thy	Mon May 09 15:00:28 2016 +0100
+++ b/thys/Paper/Paper.thy	Mon May 09 15:01:31 2016 +0100
@@ -648,9 +648,10 @@
   a case analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}. This proof requires the
   auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)
   Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily
-  established by inductions.\qed \end{proof}
+  established by inductions.\qed 
+  \end{proof}
 
-
+  \noindent
   We claim that our @{term "s \<in> r \<rightarrow> v"} relation captures the idea behind the two
   informal POSIX rules shown in the Introduction: Consider for example the
   rules @{text "P+L"} and @{text "P+R"} where the POSIX value for a string