# [isabelle] antiquotation for Isar proofs?

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?
- Gergely

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