Email Gateway (Aug 18 2022 at 12:43): Email Gateway (Aug 18 2022 at 12:43):From: John Matthews <matthews@galois.com>
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
Email Gateway (Aug 18 2022 at 12:43):From: Tobias Nipkow <nipkow@in.tum.de>
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:
Email Gateway (Aug 18 2022 at 12:44):From: Makarius <makarius@sketis.net>
This is how I usually do it, although it uses plain foiltex instead of
beamer
http://www4.in.tum.de/~wenzelm/cgi-bin/repos.cgi/Demo_Slides/archive/tip.tar.gz
Makarius
Email Gateway (Aug 18 2022 at 12:45):From: John Matthews <matthews@galois.com>
Thanks to everyone who responded to my request on incorporating
Isabelle theories into Beamer! I'm now starting to experiment with the
various approaches.
All the best,
-john
Last updated: May 03 2024 at 12:27 UTC