I sometimes see {* *} in old theory files, and find it funny to be reminded that this was standard only 5 years ago ... from my side there are no uses of this quotation remaining that I'd know of<br><br>However, (* *) is still very important for informally andquickly commenting things out, also in inner syntax!<br><br><br>Peter<div class="quote" style="line-height: 1.5"><br><br>-------- Original Message --------<br>Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?<br>From: Makarius <makarius@sketis.net><br>To: isabelle-dev <isabelle-dev@in.tum.de><br>CC: <br><br><br type="attribution"><blockquote class="quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Over the decades we have accumulated funny quotation forms in Isabelle<br>syntax that are often hard to explain to new users (also to old users).<br><br>In particular, what are the remaining uses of {* ... *}?<br><br>It should already be superseded by cartouches. There is also "isabelle<br>update_cartouches" to get rid of it (as well as `alt_string`).<br><br><br>The long-term trend is to converge to cartouches or double-quotes almost<br>everywhere. Cartouches are for nested languages, and double quotes for<br>string literals or names that are in conflict with other syntax.<br><br><br>        Makarius<br>_______________________________________________<br>isabelle-dev mailing list<br>isabelle-dev@in.tum.de<br>https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br></blockquote></div>