afl-material: coursework/cw04.tex@75c469893514 (annotated)

253 75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	1	\documentclass{article}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	2	\usepackage{../style}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	3	\usepackage{../langs}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	4
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	5	\begin{document}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	6
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	\section*{Coursework Alternative}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\noindent
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	This coursework is worth 25\% and is due on 12 December at 16:00. You are
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	asked to prove the correctness of a regular expression matcher with the
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	Isabelle theorem prover. This theorem prover is available from
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\begin{center}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\url{http://isabelle.in.tum.de}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\end{center}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\noindent
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	There is a shorte user guide for Isabelle called
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	20	``Programming and Proving in Isabelle/HOL'' at
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	21
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	22	\begin{center}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	23	\url{http://isabelle.in.tum.de/documentation.html}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	24	\end{center}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	25
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	26	\noindent
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27	and also a longer (free) book at
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\begin{center}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\url{http://www.concrete-semantics.org}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	\end{center}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	33	\noindent
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	If you need more help or you are stuck somewhere, please feel free
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	to contact me (christian.urban@kcl.ac.uk). I am a main developer of
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	Isabelle and have used it for approximately the last 14 years.
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39	\subsection*{Problem}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	\end{document}
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	43	%%% Local Variables:
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	44	%%% mode: latex
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	45	%%% TeX-master: t
75c469893514 added coursework Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	46	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Sun, 21 Sep 2014 17:40:04 +0100
changeset 253	75c469893514
child 260	65d1ea0e989f
permissions	-rw-r--r--