coursework/cw05.tex
changeset 719 0de3527e6ae3
parent 649 e83afb44f276
equal deleted inserted replaced
718:b7f9460c6a1c 719:0de3527e6ae3
     5 
     5 
     6 \begin{document}
     6 \begin{document}
     7 
     7 
     8 \section*{Coursework (Strand 2)}
     8 \section*{Coursework (Strand 2)}
     9 
     9 
    10 \noindent This coursework is worth 20\% and is due on 13 December at
    10 \noindent This coursework is worth 20\% and is due on \cwISABELLE{} at
    11 18:00. You are asked to prove the correctness of the regular expression
    11 18:00. You are asked to prove the correctness of the regular expression
    12 matcher from the lectures using the Isabelle theorem prover. You need to
    12 matcher from the lectures using the Isabelle theorem prover. You need to
    13 submit a theory file containing this proof and also a document
    13 submit a theory file containing this proof and also a document
    14 describing your proof. The Isabelle theorem prover is available from
    14 describing your proof. The Isabelle theorem prover is available from
    15 
    15