Email Gateway (Jan 02 2026 at 20:20): Email Gateway (Jan 02 2026 at 20:20):From: Tobias Nipkow <nipkow@in.tum.de>
This is how forced line breaks in mixfix annotations (eg (‹_;;//_›) used to
influence how terms are printed: @{term "c;; d"} would produce "c;; d", no line
break. In contrast, @{term [break] "c;; d"} would produce the line break after
the ;;. This was quite convenient because one had a choice. At some point in the
last few releases, the treatment of // changed and became uniform: the line
break would always be printed. What is the best way now to print terms whose
syntax contains //, without getting a line break? I have some crude latex
workaround, but there might be a better way (something like a [no_break]).
Thanks
Tobias
Last updated: Jan 11 2026 at 16:28 UTC