Re: [isabelle] Dysfunctional complete lattice syntax [was: Isabelle2016-RC0 available for testing]
On Sun, 3 Jan 2016, Florian Haftmann wrote:
The quite recent de-ASCII-fication of symbols produced a collateral
damage, illustrated with the following snippet:
term "INFIMUM A (Îx. f x x)"
The problem is that we had the tradition to add (and remove) pretty
lattice syntax by need (cf. also theory Lattice_Syntax in HOL-Library),
falling back to ASCII syntax by default.
I've recovered the former behaviour in
http://isabelle.in.tum.de/repos/isabelle/rev/fefd79f6b232 -- it relies on
the order of syntax declarations. I.e. with Main HOL with
~~/src/HOL/Library/Lattice_Syntax.thy prints proper symbols, without the
extra import it prints the old ASCII syntax.
The overall situation of syntax variants is a bit complex. I started the
inititive to swap print modes "ASCII" vs. "xsymbols" after staring at a
failed attempt to change the syntax of basic HOL connectives for more than
20min. In the longer run we should try to simplify this further.
I can forsee two solutions:
* retain ASCII syntax for INFIMUM, SUPREMUM;
* make pretty lattice syntax standard; this seems feasible since we have
syntactic type classes for all lattice operators anyway, but I guess
applications still contain definitions which do not match the type of
the polymorphic operators.
I've made a quick exploration of existing applications in Isabelle + AFP:
variants of bot/top, inf/sup, Inf/Sup, INFIMUM/SUPREMUM with symbol syntax
appear in more than one place, e.g. in HOLCF or
So it looks like one of this HOL type class reform projects that can take
weeks to get through -- i.e. something to be reconsidered after the
This archive was generated by a fusion of
Pipermail (Mailman edition) and