Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle/Isar/HOL TeX logo

Email Gateway (Aug 19 2022 at 08:17):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi all the people here,

A light topic… I was looking for a nice Isabelle/Isar and HOL logo in TeX,
and as I could not find any existing (or did I missed it?), I tried to
create a simple one, and ended with this, simple:

\newcommand{\logo}[2]{%
\raise .2ex\hbox{%
\textit{\lower .28ex\hbox{#1}}%
\hspace{-.15ex}%
\hbox{\textsmaller[3]{\textit{#2}}}%
\hspace{.15ex}%
}%
}

\newcommand{\Isar}{\logo{I}{SAR}}
\newcommand{\Isabelle}{\logo{I}{SABELLE}}
\newcommand{\HOL}{\logo{H}{OL}}

If any one with artistic or typographic inspirations has comments, these
are welcome.

I wanted to use small caps for the part following the first letter, but
italic and small‑caps does not seems to be honored, at least with
TeX‑live, neither seems to be slanted small‑caps.

Email Gateway (Aug 19 2022 at 08:17):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Forget to mention “\textsmaller” requires to “\usepackage{relsize}”.

Email Gateway (Aug 19 2022 at 08:17):

From: Alexander Krauss <krauss@in.tum.de>
[...]

Note that the standard spelling of Isabelle and Isabelle/HOL in TeX is
just "Isabelle" and "Isabelle/HOL". That is, there is no specific
branding, which merely distracts the reader. This is done consistently
in all manuals and most papers.

Alex

Email Gateway (Aug 19 2022 at 08:17):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
Two fine points, though:

1. LaTeX will by default hyphenate Isabelle as "Is-abelle", which is both unsound and incomplete w.r.t. what I could deduce from Isabella being hyphenated "I-sa-bel-la" in NOAD. Adding

   \hyphenation{i-sa-belle}

at the beginning of your document will take care of that.

2. Although linebreaks on slashes are inelegant, "Isabelle/ [linebreak] HOL" arguably looks better than "Isa- [linebreak] belle/HOL", esp. if it leads to a better balanced paragraph. To allow breaks after slashes, simply write "Isabelle\slash HOL".

Jasmin

Last updated: Nov 21 2024 at 12:39 UTC