We probably still have a few occurrences of these, but no problem phasing them out.
Cheers, Gerwin On 09.11.2018, at 10:03, Peter Lammich <lamm...@in.tum.de<mailto:lamm...@in.tum.de>> wrote: 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 However, (* *) is still very important for informally andquickly commenting things out, also in inner syntax! Peter -------- Original Message -------- Subject: [isabelle-dev] Remaining uses of {* ... *} quotation? From: Makarius To: isabelle-dev CC: Over the decades we have accumulated funny quotation forms in Isabelle syntax that are often hard to explain to new users (also to old users). In particular, what are the remaining uses of {* ... *}? It should already be superseded by cartouches. There is also "isabelle update_cartouches" to get rid of it (as well as `alt_string`). The long-term trend is to converge to cartouches or double-quotes almost everywhere. Cartouches are for nested languages, and double quotes for string literals or names that are in conflict with other syntax. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de<mailto:isabelle-...@in.tum.de> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de<mailto:isabelle-...@in.tum.de> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
