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

[Makarius]

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
description:
more abbrevs -- this makes "(=" ambiguous and thus simplifies input of
"(=)" (within the context of Main HOL);


	Makarius