coursework/cw05.tex
changeset 556 40e22ad45744
parent 500 c502933be072
child 567 4573d36d0b2f
equal deleted inserted replaced
554:2509c670e3a2 556:40e22ad45744
     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