[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


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

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

text_raw {*


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 

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,

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