# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1462802491 -3600
# Node ID fc22ca36325c54aa66754448056101f8d820f3b4
# Parent  4e3778f4a802e4fee05ae3c981f7dcaea47b07e4
updated

diff -r 4e3778f4a802 -r fc22ca36325c thys/Paper/Paper.thy
--- 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