On 3 May 2020, at 01:09, Klein, Gerwin (Data61, Kensington NSW) <[email protected]> wrote:
> I use ! all the time, esp for input (but not only for input). It’s just so > much quicker to type. Agree. We can’t repurpose (!) and there’s no need. > As I said already privately, there should then definitely be an > abbreviation for entering ∃⇩≤⇩1 using autocomplete. I could live with that… I use abbreviations all the time. Larry _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
