Email Gateway (Aug 18 2022 at 14:42): Email Gateway (Aug 18 2022 at 14:42):From: Jesper Bengtson <jesperb@it.uu.se>
Greetings all.
I'm currently trying to tweak the latex output generated by Isabelle for some formulas, and I have run into a slight problem. I'm using the @{thm [mode=Rule] ...} antiquotation, but I have a few induction rules which have premises with very many meta quantifiers. I get rules with premises which begin with
/\A B C...... X
and then the premise, the problem is that this list takes up almost half of the page, and the rest of the premise gets cramped together on the right hand side.
I am wondering if there is any way to make the list of meta quantified terms split over several rows -- the assumptions and conclusions of the premise take up several rows on their own, so this wouldn't look too bad.
I have been looking at the code which generates the Rule output, but I don't see any meta quantifiers there at all.
Best regards
/Jesper
Last updated: Apr 26 2024 at 12:28 UTC