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