[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.