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
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);
isabelle-dev mailing list