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