[isabelle-dev] [isabelle] Tiny minor backward-compatible changes to IFOL

[Klein, Gerwin (Data61, Kensington NSW)]

> On 12 May 2020, at 21:40, Makarius <makarius at sketis.net> wrote:
> 
> On 11/05/2020 14:01, Lawrence Paulson wrote:
>> Okay, I have pushed an initial version, but I think it will need a little fine-tuning. In particular, I chose the ASCII input syntax ?< on the grounds that it is impossible to type <= and therefore the ASCII syntax ?<=1 would be useless.
> 
> I see this now in Isabelle/5e315defb038.
> 
> Note that you have forgotten the NEWS entry.
> 
> 
> Are there remaining uses of ASCII replacement syntax? We have been moving away
> from it in the past couple of years, but so slowly that the move is sometimes
> hardly visible.

I’d be fine without it.


> Isabelle/jEdit provides many input methods to produce fancy notation easily
> --- preferably just one version to reduce confusion of readers of the sources.
> 
> You can declare an input abbreviation (completion) in the theory header like this:
> 
>  abbrevs Uniq = "∃⇩≤⇩1"

Yes, abbrevs is what Manuel was also suggesting. It could even be Larry's “?<“ or “?<=“ if people want that. I’m easy on this one.

Cheers,
Gerwin