[isabelle-dev] NEWS: document preparation refinements

[Makarius]

On Sat, 24 Oct 2015, Tobias Nipkow wrote:

> I don't know if this is related, but it must have happened recently: The 
> [display] option for antiquotations now (eg 436b7fe89cdc) generates latex 
> that indents the text following the display, even if there is no newline in 
> between. This is in contrast to latex conventions (eg \[ \]) and I would 
> rather not have to insert lots of \nondent by hand.

There is indeed one \n too much, which may produce an unintended 
paragraph in LaTeX.

I've changed that as follows:

changeset:   61516:8e3705d91cfa
tag:         tip
user:        wenzelm
date:        Mon Oct 26 18:04:17 2015 +0100
summary:     clarified Latex.environment (again, amending e16649b70107): 
avoid additional paragraph, e.g. relevant for option [display];


 	Makarius