coursework/cw05.tex
changeset 556 4b0fffaef849
parent 500 91b888c91d73
child 567 a48605bdf467
equal deleted inserted replaced
554:44af502ccb46 556:4b0fffaef849
     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 7 December at
     9 \noindent This coursework is worth 20\% and is due on 14 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