[isabelle-dev] Remaining uses of {* ... *} quotation?

[Makarius]

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