--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/coursework/cw04.tex	Sun Sep 21 17:40:04 2014 +0100
@@ -0,0 +1,46 @@
+\documentclass{article}
+\usepackage{../style}
+\usepackage{../langs}
+
+\begin{document}
+
+\section*{Coursework Alternative}
+
+\noindent
+This coursework is worth 25\% and is due on 12 December at 16:00. You are 
+asked to prove the correctness of a regular expression matcher with the 
+Isabelle theorem prover. This theorem prover is available from 
+
+\begin{center}
+\url{http://isabelle.in.tum.de}
+\end{center}
+
+\noindent
+There is a shorte user guide for Isabelle called 
+``Programming and Proving in Isabelle/HOL'' at
+
+\begin{center}
+\url{http://isabelle.in.tum.de/documentation.html}
+\end{center}
+
+\noindent
+and also a longer (free) book at
+
+\begin{center}
+\url{http://www.concrete-semantics.org}
+\end{center}
+
+\noindent
+If you need more help or you are stuck somewhere, please feel free
+to contact me (christian.urban@kcl.ac.uk). I am a main developer of
+Isabelle and have used it for approximately the last 14 years.
+
+
+\subsection*{Problem}
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: