<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
We probably still have a few occurrences of these, but no problem phasing them out.
<div class=""><br class="">
<div class="">
<div class="">Cheers,</div>
<div class="">Gerwin</div>
</div>
<div><br class="">
<blockquote type="cite" class="">
<div class="">On 09.11.2018, at 10:03, Peter Lammich <<a href="mailto:lammich@in.tum.de" class="">lammich@in.tum.de</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">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 class="">
<br class="">
However, (* *) is still very important for informally andquickly commenting things out, also in inner syntax!<br class="">
<br class="">
<br class="">
Peter
<div class="quote" style="line-height: 1.5"><br class="">
<br class="">
-------- Original Message --------<br class="">
Subject: [isabelle-dev] Remaining uses of {* ... *} quotation?<br class="">
From: Makarius <makarius@sketis.net class=""><br class="">
To: isabelle-dev <isabelle-dev@in.tum.de class=""><br class="">
CC: <br class="">
<br class="">
<br type="attribution" class="">
<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 class="">
syntax that are often hard to explain to new users (also to old users).<br class="">
<br class="">
In particular, what are the remaining uses of {* ... *}?<br class="">
<br class="">
It should already be superseded by cartouches. There is also "isabelle<br class="">
update_cartouches" to get rid of it (as well as `alt_string`).<br class="">
<br class="">
<br class="">
The long-term trend is to converge to cartouches or double-quotes almost<br class="">
everywhere. Cartouches are for nested languages, and double quotes for<br class="">
string literals or names that are in conflict with other syntax.<br class="">
<br class="">
<br class="">
Makarius<br class="">
_______________________________________________<br class="">
isabelle-dev mailing list<br class="">
<a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class="">
</blockquote>
</isabelle-dev@in.tum.de></makarius@sketis.net></div>
_______________________________________________<br class="">
isabelle-dev mailing list<br class="">
<a href="mailto:isabelle-dev@in.tum.de" class="">isabelle-dev@in.tum.de</a><br class="">
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev<br class="">
</div>
</blockquote>
</div>
<br class="">
</div>
</body>
</html>