> 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. But I use (*...*) to enclose arbitrary text or comment material out. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
