coursework/cw05.tex
changeset 504 5dc452d7c08e
parent 500 c502933be072
child 556 40e22ad45744
equal deleted inserted replaced
503:f2d7b885b3e3 504:5dc452d7c08e
     4 
     4 
     5 \begin{document}
     5 \begin{document}
     6 
     6 
     7 \section*{Coursework (Strand 2)}
     7 \section*{Coursework (Strand 2)}
     8 
     8 
     9 \noindent This coursework is worth 20\% and is due on 13 December at
     9 \noindent This coursework is worth 20\% and is due on 7 December at
    10 16:00. You are asked to prove the correctness of the regular
    10 16:00. You are asked to prove the correctness of the regular
    11 expression matcher from the lectures using the Isabelle theorem
    11 expression matcher from the lectures using the Isabelle theorem
    12 prover. You need to submit a theory file containing this proof. The
    12 prover. You need to submit a theory file containing this proof. The
    13 Isabelle theorem prover is available from
    13 Isabelle theorem prover is available from
    14 
    14