Re: [isabelle] Abbreviations in documents
Thanks a lot! This solved my problem.
On Tuesday, January 29, 2013 at 12:03:43 (+1100), Thomas Sewell wrote:
> 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
> 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!
> > Christian
This archive was generated by a fusion of
Pipermail (Mailman edition) and