--- a/Closures.thy	Fri Sep 02 13:34:45 2011 +0000
+++ b/Closures.thy	Fri Sep 02 14:01:11 2011 +0000
@@ -285,7 +285,6 @@
     apply(auto simp add: B_def A_def)
     apply(auto simp add: str_eq_def)
     apply(drule_tac x="CHR ''b'' ^^^ aa" in spec)
-    (*apply(auto simp add: f_def dest: l3)*)
     apply(auto)
     apply(drule_tac a="CHR ''a''" and b="CHR ''b''" in length_test)
     apply(simp add: length_test_def)

Binary file csupp.pdf has changed

--- a/csupp.tex	Fri Sep 02 13:34:45 2011 +0000
+++ b/csupp.tex	Fri Sep 02 14:01:11 2011 +0000
@@ -30,12 +30,10 @@
 \end{tabular}
 \end{center}
 \thispagestyle{empty}
-
-\section*{Background}
-
-\mbox{}\\[-14mm]
+\mbox{}\\[-5mm]
 
 \begin{multicols}{2}
+\section*{Background}
 \noindent
 Parsing is the act of transforming plain text into some
 structure that can be analysed by computers for further processing. 
@@ -45,9 +43,9 @@
 that this is not true anymore.
 
 We propose to approach the subject of parsing from a certification point 
-of view. Parsers are increasingly part of certified compilers, like CompCert, 
+of view. Parsers are increasingly part of certified compilers, like \mbox{\emph{CompCert}}, 
 which are guaranteed to be correct and bug-free. Such certified compilers are 
-important in areas where software just cannot fail. However, so far the
+crucial in areas where software just cannot fail. However, so far the
 parsers of these compilers have been left out of the certification.
 This is because parsing algorithms are often adhoc and their semantics
 is not clearly specified. Unfortunately, this means parsers can harbour 
@@ -66,7 +64,9 @@
 expressions. We like to extend this device to parsers and grammars.
 The aim is to come up with elegant and useful parsing algorithms
 whose correctness and the absence of bugs can be certified in a 
-theorem prover. 
+theorem prover.
+
+\section*{Proposed Work} 
 \mbox{}\\[15cm]
 
 \noindent