# 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)
http://www.dcs.kcl.ac.uk/staff/urbanc/cgi-bin/repos.cgi/cambridge%20tutorial/file/d866d33b15d5/T07_Latex.pdf
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)
http://www4.in.tum.de/~urbanc/cgi-bin/repos.cgi/isabelle-cookbook/raw-file/tip/progtutorial.pdf
Happy Isabelle-LaTeX hacking!
Christian

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