*** General *** * Marginal comments need to be written exclusively in the new-style form "― ‹text›", old ASCII variants like "-- {* ... *}" are no longer supported. INCOMPATIBILITY, use the command-line tool "isabelle update_comments" to update existing theory files.
* Old-style inner comments (* ... *) within the term language are legacy and will be discontinued soon: use formal comments "― ‹...›" or "⌦‹...›" instead. *** Document preparation *** * Formal comments work uniformly in outer syntax, inner syntax (term language), Isabelle/ML and some other embedded languages of Isabelle. See also "Document comments" in the isar-ref manual. The following forms are supported: - marginal text comment: ― ‹…› - canceled source: ⌦‹…› - raw LaTeX: \<^latex>‹…› *** System *** * The command-line tool "isabelle update_comments" normalizes formal comments in outer syntax as follows: ― ‹text› (whith a single space to approximate the appearance in document output). This is more specific than former "isabelle update_cartouches -c": the latter tool option has been discontinued. This refers to Isabelle/5db077cfe1b2: it is a summary of all comment-related updates, simplifications, and clarifications of the past few weeks. I have already updated the visible Isabelle universe including AFP. When old-style inner comments (* ... *) are finally discontinued, we can reunify infix notation for (+) vs. (*) etc. without extra spaces. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev