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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
