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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
