Re: [isabelle] Abbreviations in documents

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.


On 28/01/13 08:26, Christian Urban wrote:

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!

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