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

Lawrence Paulson lp15 at cam.ac.uk
Thu Nov 8 21:36:36 CET 2018


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


More information about the isabelle-dev mailing list