Email Gateway (Aug 22 2022 at 10:48): Email Gateway (Aug 22 2022 at 10:48):From: Gergely Buday <gbuday@gmail.com>
Hi,
I am thinking on writing a dictionary using the Isabelle document
preparation system.
In LaTeX the obvious choice is the glossaries package:
https://www.ctan.org/pkg/glossaries
But it is not clear how to use Isar proofs inside glossary entries:
\newglossaryentry{impthm}
{
name={important-theorem},
description={ this is an important theorem },
proof={ Isar proof here }
}
In theory an antiquotation should do it but I did not find one that
includes arbitrary Isar proof text. Is there a solution for this?
I experimented with another idea to have each glossary entry an own
Isabelle theory file but I could not specify where exactly the file
should be included in the proof document.
Writing the dictionary entries as simple sections would not give me
control of the typesetting if I want to change it for each entry
later, globally.
Do you see a neat solution here?
Last updated: Apr 25 2024 at 08:20 UTC