> On 12 May 2020, at 21:40, Makarius <[email protected]> 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 _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
