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

Manuel Eberl eberlm at in.tum.de
Sat May 2 18:28:42 CEST 2020

Do you mean "!" as an abbreviation or as actual syntax?

In case of the latter: I for one greatly prefer the one from Larry's
email greatly over "!" since it is much more evocative.


On 02/05/2020 18:02, Makarius wrote:
> On 02/05/2020 16:43, Manuel Eberl wrote:
>> Seems reasonable to me.
>> As I said already privately, there should then definitely be an
>> abbreviation for entering ∃⇩≤⇩1 using autocomplete.
> This works via 'abbrevs' in the theory header; e.g. see theory
> HOL-Library.FuncSet:
> theory FuncSet
>   imports Main
>   abbrevs PiE = "Pi\<^sub>E"
>     and PIE = "\<Pi>\<^sub>E"
> An alternative is to use "!" as originally proposed by Georgy Dunaev. My
> impression is that only the oldest users of Isabelle/FOL or HOL remember the
> historic use of "!" for universal quantification.
> With a tiny little bit of effort we could have a version of "isabelle update"
> that replaces all remaining uses of "!" automatically.
> That would be a contribution to ecology and health of features.
> 	Makarius

More information about the isabelle-dev mailing list