Re: [isabelle] Abbreviations in documents




Thanks a lot! This solved my problem.

Christian

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 
 > documents.
 > 
 > Yours,
 >      Thomas.
 > 
 > 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 MHonArc.