Email Gateway (Mar 31 2023 at 08:19): Email Gateway (Mar 31 2023 at 08:19):From: Tobias Nipkow <nipkow@in.tum.de>
When two text-blocks directly follow one another in an Isabelle thy, the
generated document will have some additional space between them. Is there some
reliable way to remove that?
(I would love to collapse two such consecutive text blocks into one, but if one
of them is (in locale), I cannot do that. There used to be the option of adding
(in locale) to individual antiquitations, which would solve my problem, but I
don't think that is still possible.)
Similarly, if I do
\input{Thy1]
\input{Thy2}
in a latex file to include the tex files generated by Thy1.thy and Thy2.thy,
there is additional space between them.
Tobias
Last updated: Apr 19 2024 at 04:17 UTC