Re: [isabelle] Document preparation question

On Thursday, January 17, 2013 at 10:19:30 (+0100), Joachim Breitner wrote:
 > Sometimes the lemmas would be clearer if free variables were explicitly
 > all-quantified. Is there an easy way to achieve this (besides defining a
 > variant of the lemma with an HOL-∀ in front)?

This is possible, but you would need to write
your own theorem-style. Some time ago I gave
an Isabelle-LaTeX-hacking talk, where as an
example I demonstrated the opposite, i.e. printing 
a forall-quantified theorem without the quantifiers. 
Have a look at the slides (pages 10pp) 
Essentially what you need to do is to manipulate
the term underlying the theorem. There are also a 
few rough notes about document anti-quotations
here (page 187spp)

Happy Isabelle-LaTeX hacking!


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