coursework/cw05.tex
changeset 500 c502933be072
parent 419 4110ab35e5d8
child 556 40e22ad45744
equal deleted inserted replaced
499:dfd0f41f8668 500:c502933be072
     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