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

[Lawrence Paulson]

> 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.

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