Email Gateway (Jan 28 2025 at 14:52): Email Gateway (Jan 28 2025 at 14:52):From: Makarius <makarius@sketis.net>
* Inner syntax --- the term language *
Former theory "HOL-Library.Adhoc_Overloading" is now included in Pure,
with a few changes (minor INCOMPATIBILITY):
Theory imports of "HOL-Library.Adhoc_Overloading" need to be removed
(or replaced by Main).
Equivalence of overloaded constants has become more liberal: sorts
of type variables are ignored, schematic type variables only need to
match (in both directions) instead of being literally equal.
Command syntax now requires a separator: "adhoc_overloading c ⇌ vs".
The "no" keyword for bundles works as for 'syntax' / 'no_syntax'.
This refers to Isabelle/7301923ad1e9 and AFP/3b6522ae5f77.
The move from HOL-Library to Pure has several motivations:
* reconcile the fork
thys/Transport/HOL_Basics/Adhoc_Overloading/Adhoc_Overloading.thy (e.g.
AFP/e69d71bc07c4)
* eventually integrate it better with term abbreviations and class
declaration context
* eventually use adhoc_overloading in Main HOL (not now, and not for this
release)
(Thanks to our great new Build_Manager, this change required only 1 day total,
instead of several days waiting for test builds.)
Makarius
Last updated: Mar 07 2025 at 20:20 UTC