Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Abbreviations in documents

Email Gateway (Aug 19 2022 at 09:42):

From: Christian Urban <christian.urban@kcl.ac.uk>
Dear All,

I have a formalisation where I am using an
abbreviation for a logic formula, like

some_abbr == (%t. t = something_else)

In my document however I prefer to show my
theorems involving this abbreviation in
the "unfolded" way. Is it possible to
somehow unfold abbreviations in documents?

Thanks a lot!
Christian

Email Gateway (Aug 19 2022 at 09:44):

From: Thomas Sewell <Thomas.Sewell@nicta.com.au>
A useful approximation to this may be the (input) option to
abbreviation, e.g.

abbreviation (input)
"some_abbr == (%t. t = some_expr)"

That abbreviation will be available for parsing your text but won't be
used in printing. Generally handy. I'm fairly sure it won't be used in
documents.

Yours,
Thomas.

Email Gateway (Aug 19 2022 at 09:45):

From: Christian Urban <christian.urban@kcl.ac.uk>
Thanks a lot! This solved my problem.

Christian

Last updated: Apr 19 2024 at 04:17 UTC