# [isabelle] Isabelle and Beamer

Hi Matthew,

> I'm thinking of trying out the Beamer class to make some LaTeX slides
> containing selected definitions and lemmas from some of my Isabelle
> theory files. Does anyone have some advice on the best way to go about
> this?

I am using this combination routinely for my slides. See

http://www4.in.tum.de/~urbanc/Teaching/isabelle08.html

Isabelle code starts at page 10 on the first set of slides.

On the whole there is nothing special about Beamer and Isabelle.
You include the Beamer-Package in root.tex with

\documentclass{beamer}

and the Beamer-styles with \usepackage. You can then generate
Slides inside a theory file using

text_raw {*
\mode<presentation>{
\begin{frame}
\frame{title{.....}

\end{frame}}
*}

You need to use text_raw, if you want to mix LateX-code with
Isabelle code.

Unfortunately, by default the Isabelle code will be shown only in
black-and-white, just like in normal documents. I think this is not
appropriate for slides. Therefore I use a simple Perl-hack by Alexander
Krauss to colour the Isabelle code after it has been generated by
Isabelle.

I am very happy with this way of generating slides (because it is
very fast). If you want I can send you my slides and associated files.

Best wishes,
Christian



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.