Hi,
Up until Isabelle2018, I used (* ... *) to comment out parts of
lemmas/definitions, mostly for debugging larger expressions.
Highlighted in red, (* ... *) was nicely set apart from the rest of the
expression.
Now (e.g., isabelle/b58a575d211e) we can use \<^cancel>, but its
"highlighting"
Hi FabianI already pointed out the missing highlighting of cancel a few months ago ... I am still strongly in favor of having a highlighting that can easily be distinguished, eg the legacy red, or perhaps gray ...Right now, when using Isabelle 2018, I do not use cancel, but (**), getting a warning,
Oh, you are right - there was a thread about that on isabelle-users in
July/August/November, e.g.:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-July/msg00124.html
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2018-August/msg00146.html
https://lists.cam.ac.uk/pipermail/cl-isabell