theory Exercise01
imports Main
begin

text {*

\begin{itemize}
\item
  Switch on X-Symbol in ProofGeneral.

\item
  Make yourself familiar with the editing facilities of XEmacs.
\item
  Help $\to$ Commands \& Keys $\to$ Bindings lists currenty key bindings.

\item
  Step through the demo file from the lecture web page.

\item
  Write an own theory file, look at some theorems in the library,
  try 'find theorem'.

\item
  With the help of Appendix A of the tutorial, enter some first-order
  conjectures in your theory file.

\item
  Generate a pdf for the second exercise sheet \texttt{Example02.thy}.

\item
  Generate a pdf from your theory file.
\end{itemize}

*}

end