Email Gateway (Feb 04 2025 at 22:09): Email Gateway (Feb 04 2025 at 22:09):From: David <davfuenmayor@gmail.com>
Dear Makarius/developers,
I saw this issue has been recently mentioned, but I still cannot figure out
the correct way (as in intended by developers) to hide syntax/notation in
the new Isabelle version. For instance:
Before (Isabelle2024):
no_notation Set.subset ("'(⊂')") and Set.subset ("(_/ ⊂ _)" [51, 51] 50)
Now (Isabelle2025):
???
Thanks and best regards
David
Email Gateway (Feb 06 2025 at 20:02):From: Makarius <makarius@sketis.net>
On 04/02/2025 23:09, David wrote:
Dear Makarius/developers,
I saw this issue has been recently mentioned, but I still cannot figure out
the correct way (as in intended by developers) to hide syntax/notation in the
new Isabelle version. For instance:Before (Isabelle2024):
no_notation Set.subset ("'(⊂')") and Set.subset ("(_/ ⊂ _)" [51, 51] 50)Now (Isabelle2025):
???
Now is Isabelle2025-RC1, not yet Isabelle2025.
The 'no_syntax' and 'no_notation' commands themselves did not change: you need
to specify the syntax clauses precisely as in the original 'syntax' and
'notation' commands of the underlying library theories. The latter has changed
in many situations, see this explanation in NEWS:
"""
The recommendation to "use unbundle no foobar_syntax" depends on the library
providing such bundles, e.g. via 'open_bundle'. I have introduced several such
bundles for syntax that is likely to be replaced, according to things seen in
AFP. If no suitable bundle is available, you need to copy-paste suitable parts
from the original syntax specifications, as before. This is a bit fragile, of
course.
Alternatively, you can make a convincing argument, which additional syntax
bundles should be added now, before Isabelle2025 is finalized.
Concerning basic notation of HOL predicate logic and sets, I would say that
applications should rather not touch that. We already have the \<^bold>
control-symbol to introduce copies of popular symbols without causing conflicts.
So now we at the usual meta-question: What are you trying to do? What is your
application?
Makarius
Email Gateway (Feb 11 2025 at 23:17):From: David <davfuenmayor@gmail.com>
Thanks for your answer!
Alternatively, you can make a convincing argument, which additional syntax
bundles should be added now, before Isabelle2025 is finalized.
I would argue for the following two syntax bundles:
1) All syntax introduced in HOL libraries that goes beyond the basic HOL
logical connectives (i.e. boolean operators, quantifiers, descriptions &
co).
2) All syntax at all (not even HOL connectives, though maybe
equality/disequality symbols may remain).
My (convincing?) argument is to allow for users working on "vanilla HOL"
(i.e. STLC + equality; cf. Andrews system Q) to use Isabelle as their proof
editor.
Such users often need to provide their own custom versions of basic
libraries, both for pedagogical and pragmatic ATP-related reasons.
In my case, I do not use anything from the Isabelle libraries (well,
indirectly the things required by auto, metis, nitpick & co. to work).
So now we at the usual meta-question: What are you trying to do? What is
your
application?
Right now I am developing a library with use in (shallow) encodings of
modal and non-classical logics (
https://github.com/davfuenmayor/logic-bricks/).
I provide there my own libraries for sets, relations, etc., and often
struggle with syntax collisions with the Isabelle/HOL library.
Best
David
On Thu, Feb 6, 2025 at 9:01 PM Makarius <makarius@sketis.net> wrote:
On 04/02/2025 23:09, David wrote:
Dear Makarius/developers,
I saw this issue has been recently mentioned, but I still cannot figure
out
the correct way (as in intended by developers) to hide syntax/notation
in the
new Isabelle version. For instance:Before (Isabelle2024):
no_notation Set.subset ("'(⊂')") and Set.subset ("(_/ ⊂ _)" [51, 51]
50)Now (Isabelle2025):
???Now is Isabelle2025-RC1, not yet Isabelle2025.
The 'no_syntax' and 'no_notation' commands themselves did not change: you
need
to specify the syntax clauses precisely as in the original 'syntax' and
'notation' commands of the underlying library theories. The latter has
changed
in many situations, see this explanation in NEWS:"""
* Blocks in mixfix annotations now support properties [...]
Occasional INCOMPATIBILITY for 'no_syntax' or 'no_notation'
declarations in user applications: the mixfix template needs to be
adapted accordingly, but it is often better to use "unbundle no
foobar_syntax", as explained for HOL libraries below.
"""The recommendation to "use unbundle no foobar_syntax" depends on the
library
providing such bundles, e.g. via 'open_bundle'. I have introduced several
such
bundles for syntax that is likely to be replaced, according to things seen
in
AFP. If no suitable bundle is available, you need to copy-paste suitable
parts
from the original syntax specifications, as before. This is a bit fragile,
of
course.Alternatively, you can make a convincing argument, which additional syntax
bundles should be added now, before Isabelle2025 is finalized.Concerning basic notation of HOL predicate logic and sets, I would say
that
applications should rather not touch that. We already have the \<^bold>
control-symbol to introduce copies of popular symbols without causing
conflicts.So now we at the usual meta-question: What are you trying to do? What is
your
application?Makarius
Last updated: Mar 09 2025 at 12:28 UTC