[isabelle] antiquotation for Isar proofs?


I am thinking on writing a dictionary using the Isabelle document
preparation system.

In LaTeX the obvious choice is the glossaries package:


But it is not clear how to use Isar proofs inside glossary entries:

 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.