[isabelle] Abbreviations in documents




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.