On Mon, 2 Sep 2013, Makarius wrote:
I find myself using the "iff" notation most of the time to make theories
look "nice".
Are there clubs of "iff" vs. "non-iff"? If almost everybody is a member of
the "iff" club we could just remove that print mode.
I've forgotten to point out the relationship to this isabelle-users
thread about "Isabelle operator precedence":
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-November/msg00020.html
Part of it was some confusion about "infixl" vs. "infix" of HOL eq and
not_equal, which was coming from a bit too many variants being there, and
some of them not quite right (it is probably right at
Isabelle/b46e6cd75dc6).
Back then I wrote:
I think the "=" notation is going back to a time even before the
'infixl' / 'infixr' macros for the general mixfix form, and there were also
some
special tweaks for output and breaks unlike regular infixes. 'infix' is
much younger than all that.
In the last 10 years, there have been some slight reforms towards more
regularity of notation for eq/not_equal in HOL. It might be worth trying
again to make it all just plain infix 50, although just from the
ancienticity of it it could cause some surprises in some dark corners.
Trying the latter, i.e. using just plain infix 50 for = and its negated
version, reveals problems rather early. For example in Set.thy:
lemma subset_eq [no_atp]: "A ≤ B = (∀x∈A. x ∈ B)" by blast
So any of the infixes with priority 50 will cause problems that do not
exist with the iff notation, since that has weaker priority. The latter
also allows to remove many parentheses.
The above example also has ≤ instead of ⊆ for sets, which is somehow
related. (Continuing that train of thought will inevitably expose cans of
worms, so this speculative thread is definitely not relevant for the
coming release.)
Makarius_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
