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.