Re: [isabelle] Isabelle and Beamer



I have done this and it worked quite well. I had a file main.tex with latex/beamer source in it. At certain places I would include one or more slides via \input{Slides/generated/XYZ.tex} where Slides is a subdirectory containing theories with Isabelle-specific beamer slides. One such theory would be XYZ.thy, and when I "make" Slides the result would be put into the subdirectory "generated". Theory XYZ would look like this:

(*<*)
theory XYZ ...
begin
(*>*)

text{*

\begin{frame}
...
\end{frame}

...

*}

(*<*)
end
(*>*)

Hope that helps
Tobias


John Matthews wrote:
Hi,

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?

Thanks,
-john







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