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

[Makarius]

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.

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"

It also shows up in the "Symbols" panel, in group "Abbrevs", which is the
first one that is open by default.


	Makarius