coursework/cw05.tex
changeset 649 e83afb44f276
parent 630 9b1c15c3eb6f
child 719 0de3527e6ae3
equal deleted inserted replaced
648:36379b038438 649:e83afb44f276
     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 13 December at
    11 18:00. You are asked to prove the correctness of the regular
    11 18:00. You are asked to prove the correctness of the regular expression
    12 expression matcher from the lectures using the Isabelle theorem
    12 matcher from the lectures using the Isabelle theorem prover. You need to
    13 prover. You need to submit a theory file containing this proof. The
    13 submit a theory file containing this proof and also a document
    14 Isabelle theorem prover is available from
    14 describing your proof. The Isabelle theorem prover is available from
    15 
    15 
    16 \begin{center}
    16 \begin{center}
    17 \url{http://isabelle.in.tum.de}
    17 \url{http://isabelle.in.tum.de}
    18 \end{center}
    18 \end{center}
    19 
    19