coursework/cw05.tex
changeset 649 e83afb44f276
parent 630 9b1c15c3eb6f
child 719 0de3527e6ae3
--- a/coursework/cw05.tex	Mon Oct 07 20:53:25 2019 +0100
+++ b/coursework/cw05.tex	Tue Oct 08 21:12:52 2019 +0100
@@ -8,10 +8,10 @@
 \section*{Coursework (Strand 2)}
 
 \noindent This coursework is worth 20\% and is due on 13 December at
-18:00. You are asked to prove the correctness of the regular
-expression matcher from the lectures using the Isabelle theorem
-prover. You need to submit a theory file containing this proof. The
-Isabelle theorem prover is available from
+18:00. You are asked to prove the correctness of the regular expression
+matcher from the lectures using the Isabelle theorem prover. You need to
+submit a theory file containing this proof and also a document
+describing your proof. The Isabelle theorem prover is available from
 
 \begin{center}
 \url{http://isabelle.in.tum.de}