# HG changeset patch
# User urbanc
# Date 1314972071 0
# Node ID 87a8dc29d7ae7eb7e4ec29ab9e47b3efc5e33dad
# Parent  9c281a4b767ddf6f736611c875386e51ad4effe8
latest changes

diff -r 9c281a4b767d -r 87a8dc29d7ae Closures.thy
--- 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)
diff -r 9c281a4b767d -r 87a8dc29d7ae csupp.pdf
Binary file csupp.pdf has changed
diff -r 9c281a4b767d -r 87a8dc29d7ae csupp.tex
--- 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