On 08/11/2018 21:36, Lawrence Paulson wrote:
>> On 8 Nov 2018, at 20:32, Makarius <makar...@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
LaTeX).
Proper document text would normally appear within cartouches and marked
by 'text' or \<comment>.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
