[isabelle-dev] NEWS: op <infix> -> (<infix>)

Makarius makarius at sketis.net
Wed Mar 7 19:25:55 CET 2018

On 06/03/18 16:04, Peter Lammich wrote:
> I observed that "(=)" is hard to type in the default symbols setup, it
> will be folded to "\<subseteq>)" if immediate completion is on (A short
> informal poll in our group resulted that most of us have immediate
> completion on).

Of course, the default setup needs to work as smoothly as possible,
independently of the number of people who might opt in or out from it.

> Is it possible to keep (= bound to \<subseteq>, but exclude it from
> immediate completion?

In such situations the usual approach is to make the abbreviation
ambiguous: that forces a popup to be produced.

I've now done this by introducing some further abbrevs for "(=" that are
actually useful:

changeset:   67780:7655e6369c9f
tag:         tip
user:        wenzelm
date:        Wed Mar 07 19:02:22 2018 +0100
files:       src/HOL/Library/Finite_Map.thy src/HOL/Map.thy
more abbrevs -- this makes "(=" ambiguous and thus simplifies input of
"(=)" (within the context of Main HOL);


More information about the isabelle-dev mailing list