[isabelle-dev] Remaining uses of {* ... *} quotation?

Makarius makarius at sketis.net
Fri Nov 9 12:24:42 CET 2018

On 08/11/2018 21:36, Lawrence Paulson wrote:
>> On 8 Nov 2018, at 20:32, Makarius <makarius at sketis.net> wrote:
>> In particular, what are the remaining uses of {* ... *}?
> I didn’t even know that existed.

It was used a lot with the 'section' and 'text' commands until recently.
That was actually its main motivation approx. 20 years ago: to delimit
LaTeX sources reliably.

Now the occurrence of {* ... *} in some existing sources makes them look
very old-fashioned, but "isabelle update_cartouches -t" does a thorough
job automatically.

> But I use (*...*) to enclose arbitrary text or comment material out.

Outer comment syntax will remain unchanged: its main purpose is to
comment-out material temporarily, or to write meta-comments (like % in

Proper document text would normally appear within cartouches and marked
by 'text' or \<comment>.


More information about the isabelle-dev mailing list