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 https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev