Will there still be a way to comment out random junk? I often work with a mixture of Isabelle and commented-out HOL Light material.
Larry > On 26 Jan 2018, at 20:19, Makarius <makar...@sketis.net> wrote: > > * Old-style inner comments (* ... *) within the term language are legacy > and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›" > instead.
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
