[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.