Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] LaTeX packages for greek and italicized letters

Email Gateway (Mar 26 2025 at 20:33):

From: Pasquale Noce <pasquale.noce.lavoro@gmail.com>
Dear Isabelle users,

Which LaTeX packages do I need to include in my root.tex file to enable my
document to contain the greek and italicized letters from tabs "Greek" and
"Letter" of the "Symbols" panel - I mean, to make PDF document generation
work?
I apologize for asking a so trivial question, but I am by no means a LaTeX
expert, so your help would be much appreciated.

Thank you very much, best regards,
Pasquale Noce

Email Gateway (Mar 26 2025 at 21:13):

From: Makarius <makarius@sketis.net>
On 26/03/2025 21:32, Pasquale Noce wrote:

Which LaTeX packages do I need to include in my root.tex file to enable my
document to contain the greek and italicized letters from tabs "Greek" and
"Letter" of the "Symbols" panel - I mean, to make PDF document generation
work?

If you mean formal Isabelle symbols like \<alpha> in your informal text, you
merely need to ensure that you embed them into formal antiquotations. The most
basic antiquotation is called @{text} or @{cartouche}, but we stopped using
this archaic notation many years ago. Instead, you now write @{cartouche "α"}
with literal cartouche notation as ‹α›.

Here is an example:

theory Test imports Main
begin

text ‹
▪ informal text: blah
▪ formal text: ‹α›
›

end

Other notable antiquotations are @{typ} @{term} @{thm} --- usually written as
\<^term>‹α› etc.

Makarius

Last updated: Apr 17 2025 at 20:22 UTC