1 \documentclass{article}

     2 \usepackage{../style}

     3 \usepackage{../langs}

     4 

     5 \begin{document}

     6 

     7 \section*{Coursework Alternative}

     8 

     9 \noindent

    10 This coursework is worth 25\% and is due on 12 December at 16:00. You are 

    11 asked to prove the correctness of a regular expression matcher with the 

    12 Isabelle theorem prover. This theorem prover is available from 

    13 

    14 \begin{center}

    15 \url{http://isabelle.in.tum.de}

    16 \end{center}

    17 

    18 \noindent

    19 There is a shorte user guide for Isabelle called 

    20 ``Programming and Proving in Isabelle/HOL'' at

    21 

    22 \begin{center}

    23 \url{http://isabelle.in.tum.de/documentation.html}

    24 \end{center}

    25 

    26 \noindent

    27 and also a longer (free) book at

    28 

    29 \begin{center}

    30 \url{http://www.concrete-semantics.org}

    31 \end{center}

    32 

    33 \noindent

    34 If you need more help or you are stuck somewhere, please feel free

    35 to contact me (christian.urban@kcl.ac.uk). I am a main developer of

    36 Isabelle and have used it for approximately the last 14 years.

    37 

    38 

    39 \subsection*{Problem}

    40 

    41 \end{document}

    42 

    43 %%% Local Variables: 

    44 %%% mode: latex

    45 %%% TeX-master: t

    46 %%% End: