[isabelle] Remaining use of {* ... *}

On Tue, 26 Aug 2014, Gottfried Barrow wrote:

There is one huge surface addition, and that's \<open> and \<closed>. Those are huge, because they're subtle and graphical, and they help to clearly delimit the beginning and end of text, better than {* and *}, though those have their use.

Just the canonical question: What is the remaining use of {* ... *} here?

It won't go away, but might eventually be superseded by \<open> ... \<close> (which is rendered in Unicode as as ‹...› with some input method in the Prover IDE via single backquote).

I am myself using mainly ‹...› since a few months and it should be easy to make an Isabelle/Scala function to replace outer syntax {* ... *} systematically in existing Isabelle projects.

At UITP 2014, Andrew Butterfield briefly referred to Isabelle/UTP http://www-users.cs.york.ac.uk/~simonf/utp-isabelle in comparison to his own UTP proof assistant. He made a funny rant about "terms in double quotes with double single quotes to quote UTP within HOL". Moving more and more towards cartouches ‹...› would make the nesting of Isabelle languages more regular.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.