Email Gateway (Apr 22 2026 at 09:47): Email Gateway (Apr 22 2026 at 09:47):From: Lawrence Paulson <lp15@cam.ac.uk>
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?
Larry
Email Gateway (Apr 22 2026 at 09:54):From: Makarius <makarius@sketis.net>
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?
Which changeset of isabelle-dev do you actuall mean?
Alternatives are bad and make Isabelle hard to use and hard to learn.
Which other alternatives are on the list of removal, for a bright and happy
future of Isabelle?
Makarius
Email Gateway (Apr 22 2026 at 10:08):From: Lawrence Paulson <lp15@cam.ac.uk>
changeset: 83876:0b1311a82548
Retaining the minus sign (-) for input but displaying a special symbol is exactly how we treat many other ASCII operators, such as &, |, :, Un.
Larry
On 22 Apr 2026, at 10:53, Makarius <makarius@sketis.net> wrote:
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?Which changeset of isabelle-dev do you actuall mean?
Alternatives are bad and make Isabelle hard to use and hard to learn.
Which other alternatives are on the list of removal, for a bright and happy future of Isabelle?
Email Gateway (Apr 22 2026 at 10:11):From: Manuel Eberl <manuel@pruvisto.org>
I noticed it and was a bit surprised at the change (after all those
years). But I'm not against it; I'd say I'm neutral. It's closer to
mathematical notation, and therefore I also think the potential for
confusion is probably not that big.
There is arguably also some inconsistency that "+" on sets is either a
type error or pointwise addition (depending on whether you import the
corresponding HOL-Library theory), whereas "-" is not pointwise
subtraction but set difference. Not a big problem, of course, and the
present change does not address that problem either (but it can be seen
as a first step towards addressing it).
TL;DR It's not something I would have done but I am not against it.
Which other alternatives are on the list of removal, for a bright and
happy future of Isabelle?
Assuming that you're not talking about set difference but in general:
There is a whole bunch of antiquated syntax for limits and derivatives
that we probably inherited from HOL Light. Stuff like "DERIV f x :> f'"
for "(f has_field_derivative f') (at x)" (and the same for FDERIV and
possibly a few more) or "LIM x F. f :> G" for "filterlim (λx. f) G F".
Many theorem names also still have "DERIV" in them.
Manuel
On 22/04/2026 11:53, Makarius wrote:
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in
mathematics the standard notation is A∖B. recently, in the
development version, I changed the default operator to ∖ while
retaining the minus sign as an alternative for input. So it is an
upwards compatible change but possibly confusing to some users. Note
in particular that the \ character on your keyboard does not generate
the right symbol; you have to select it from a pallet or type \setminus.Thoughts/reactions?
Which changeset of isabelle-dev do you actuall mean?
Alternatives are bad and make Isabelle hard to use and hard to learn.
Which other alternatives are on the list of removal, for a bright and
happy future of Isabelle?Makarius
Email Gateway (Apr 22 2026 at 10:12):From: Tobias Nipkow <nipkow@in.tum.de>
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?
I prefer "-" because it is easier to type, and we should retain it.
I find that \<setminus> invites confusion with \ (as you pointed out)
and I don'tlike the look of \<setminus> which is a bit faint
(probably to distinguish it from \)
But I won't stand in the way of progress if there is strong support for it.
Tobias
Larry
Email Gateway (Apr 22 2026 at 10:14):From: Manuel Eberl <manuel@pruvisto.org>
As I understand it, Makarius wants to move away from that as well. And I
think it makes sense. This stuff is pretty confusing and, in my opinion,
unnecessary. No one types it that way these days and it'd be good to
have consistent notation. This ASCII syntax for ∧ etc. reminds me of the
old digraphs and trigraphs from C.
Manuel
On 22/04/2026 12:07, Lawrence Paulson wrote:
changeset: 83876:0b1311a82548
Retaining the minus sign (-) for input but displaying a special symbol is exactly how we treat many other ASCII operators, such as &, |, :, Un.
Larry
On 22 Apr 2026, at 10:53, Makarius <makarius@sketis.net> wrote:
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?
Which changeset of isabelle-dev do you actuall mean?Alternatives are bad and make Isabelle hard to use and hard to learn.
Which other alternatives are on the list of removal, for a bright and happy future of Isabelle?
Email Gateway (Apr 22 2026 at 10:17):From: Lawrence Paulson <lp15@cam.ac.uk>
These date from the 1990s, when Jacques Fleuriot developed the reals and limits, etc., for the first time. But I agree, these old notations are confusing.
Larry
On 22 Apr 2026, at 11:10, Manuel Eberl <manuel@pruvisto.org> wrote:
There is a whole bunch of antiquated syntax for limits and derivatives that we probably inherited from HOL Light. Stuff like "DERIV f x :> f'" for "(f has_field_derivative f') (at x)" (and the same for FDERIV and possibly a few more) or "LIM x F. f :> G" for "filterlim (λx. f) G F". Many theorem names also still have "DERIV" in them.
Email Gateway (Apr 22 2026 at 10:20):From: Tobias Nipkow <nipkow@in.tum.de>
I constantly use the shorthands for selecting the corresponding \<...> symbol.
Tobias
On 22/04/2026 12:14, Manuel Eberl wrote:
As I understand it, Makarius wants to move away from that as well. And I think
it makes sense. This stuff is pretty confusing and, in my opinion, unnecessary.
No one types it that way these days and it'd be good to have consistent
notation. This ASCII syntax for ∧ etc. reminds me of the old digraphs and
trigraphs from C.Manuel
On 22/04/2026 12:07, Lawrence Paulson wrote:
changeset: 83876:0b1311a82548
Retaining the minus sign (-) for input but displaying a special symbol is
exactly how we treat many other ASCII operators, such as &, |, :, Un.Larry
On 22 Apr 2026, at 10:53, Makarius <makarius@sketis.net> wrote:
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics
the standard notation is A∖B. recently, in the development version, I
changed the default operator to ∖ while retaining the minus sign as an
alternative for input. So it is an upwards compatible change but possibly
confusing to some users. Note in particular that the \ character on your
keyboard does not generate the right symbol; you have to select it from a
pallet or type \setminus.
Thoughts/reactions?
Which changeset of isabelle-dev do you actuall mean?Alternatives are bad and make Isabelle hard to use and hard to learn.
Which other alternatives are on the list of removal, for a bright and happy
future of Isabelle?
Email Gateway (Apr 22 2026 at 10:22):From: Manuel Eberl <manuel@pruvisto.org>
Yes, but that is completely orthogonal to what syntax we allow in the
actual terms. For example, "?" autocompletes to "∃" but if you write
"?x. P x" you get a syntax error. ("!x. P x" still works; it's a bit
inconsistent)
Manuel
On 22/04/2026 12:20, Tobias Nipkow wrote:
I constantly use the shorthands for selecting the corresponding \<...>
symbol.Tobias
On 22/04/2026 12:14, Manuel Eberl wrote:
As I understand it, Makarius wants to move away from that as well.
And I think it makes sense. This stuff is pretty confusing and, in my
opinion, unnecessary. No one types it that way these days and it'd be
good to have consistent notation. This ASCII syntax for ∧ etc.
reminds me of the old digraphs and trigraphs from C.Manuel
On 22/04/2026 12:07, Lawrence Paulson wrote:
changeset: 83876:0b1311a82548
Retaining the minus sign (-) for input but displaying a special
symbol is exactly how we treat many other ASCII operators, such as
&, |, :, Un.Larry
On 22 Apr 2026, at 10:53, Makarius <makarius@sketis.net> wrote:
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in
mathematics the standard notation is A∖B. recently, in the
development version, I changed the default operator to ∖ while
retaining the minus sign as an alternative for input. So it is an
upwards compatible change but possibly confusing to some users.
Note in particular that the \ character on your keyboard does not
generate the right symbol; you have to select it from a pallet or
type \setminus.
Thoughts/reactions?
Which changeset of isabelle-dev do you actuall mean?Alternatives are bad and make Isabelle hard to use and hard to learn.
Which other alternatives are on the list of removal, for a bright
and happy future of Isabelle?
Email Gateway (Apr 22 2026 at 10:59):From: Makarius <makarius@sketis.net>
On 22/04/2026 12:07, Lawrence Paulson wrote:
changeset: 83876:0b1311a82548
That says "A few useful results from AFP entries". So it looks like an
accident, especially since there is no related NEWS entry.
Retaining the minus sign (-) for input but displaying a special symbol is exactly how we treat many other ASCII operators, such as &, |, :, Un.
These are on my list of removal, for so many decades.
The plan is to keep them as input methods only. But I did not start the
process yet to ask "What are remaining uses of ASCII replacement syntax".
Makarius
Email Gateway (Apr 22 2026 at 11:13):From: Makarius <makarius@sketis.net>
On 22/04/2026 12:12, Tobias Nipkow wrote:
I prefer "-" because it is easier to type, and we should retain it.
I find that \<setminus> invites confusion with \ (as you pointed out)
and I don'tlike the look of \<setminus> which is a bit faint
(probably to distinguish it from \)But I won't stand in the way of progress if there is strong support for it.
"Progress" could also mean "progressive decay".
I am against even more alternatives. They multiply and an produce exponential
confusion.
Makarius
Email Gateway (Apr 23 2026 at 09:26):From: Makarius <makarius@sketis.net>
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?
See also this thread 09-Feb-2024 from
https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2024-02/msg00021.html ---
when there was a more activity on this channel, and less enthusiasm about the
idea.
If you still want to hold up the proposal: What is your plan to upgrade the
large body of existing sources? What kind of tool would you build for that?
Makarius
Email Gateway (Apr 23 2026 at 10:11):From: Lawrence Paulson <lp15@cam.ac.uk>
People don't seem to care very much, so maybe we should leave things out as they are.
On 23 Apr 2026, at 10:25, Makarius <makarius@sketis.net> wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?See also this thread 09-Feb-2024 from https://lists.cam.ac.uk/sympa/arc/cl-isabelle-users/2024-02/msg00021.html--- when there was a more activity on this channel, and less enthusiasm about the idea.
If you still want to hold up the proposal: What is your plan to upgrade the large body of existing sources? What kind of tool would you build for that?
Email Gateway (Apr 23 2026 at 13:06):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
What are opinions concerning = for <-->?
Stepan
On 22-Apr-26 11:46 AM, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?
Larry
Email Gateway (May 04 2026 at 18:59):From: Makarius <makarius@sketis.net>
On 22-Apr-26 11:46 AM, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics
the standard notation is A∖B. recently, in the development version, I
changed the default operator to ∖ while retaining the minus sign as an
alternative for input. So it is an upwards compatible change but possibly
confusing to some users. Note in particular that the \ character on your
keyboard does not generate the right symbol; you have to select it from a
pallet or type \setminus.Thoughts/reactions?
On 23/04/2026 15:06, Stepan Holub (via cl-isabelle-users Mailing List) wrote:
What are opinions concerning = for <-->?
That is indeed a better model for the proposed change, because it "improves"
on a regular notation for specific types: equality on type bool becomes
logical equivalence as separate notation. So it is not about ASCII replacement
syntax, but type-specific improvement of notation.
The implementation is notable in providing a "print_mode": only with that mode
enable is the alternative form used for output. Thus it is a bit less
intrusive: at least in principle it can be controlled by the user. (Print
modes have become a bit out-of-fashion, but maybe could be brushed up by
supporting them within syntax bundles.)
BTW, "the latest repository version" has more software entropy here:
changeset: 84567:05a7b85c80ed
parent: 84561:b28eb0ace0a1
user: paulson <lp15@cam.ac.uk>
date: Mon May 04 17:47:41 2026 +0100
files: src/HOL/Analysis/Infinite_Products.thy src/HOL/Set.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
description:
Reverting a couple of changes
Maybe Larry can explain the plan, if there is any.
The log entry is invalid, because some of the changes are newly introduced,
and not reverting earlier ones. (When reading the history later, it needs to
explain why things were done that way.)
Makarius
Email Gateway (May 04 2026 at 19:21):From: Makarius <makarius@sketis.net>
On 22/04/2026 11:46, Lawrence Paulson wrote:
In Isabelle we’ve always written A-B for set difference, but in mathematics the standard notation is A∖B. recently, in the development version, I changed the default operator to ∖ while retaining the minus sign as an alternative for input. So it is an upwards compatible change but possibly confusing to some users. Note in particular that the \ character on your keyboard does not generate the right symbol; you have to select it from a pallet or type \setminus.
Thoughts/reactions?
A few days ago I've attended a talk about "jj", an emerging successor to git
(which many people now consider as "stuck" and don't give it another 20 years
of dominance).
The jj "revset language" https://docs.jj-vcs.dev/latest/revsets uses the funny
notation "A ~ B" for set-minus.
Makarius
Last updated: May 23 2026 at 03:31 UTC