NEWS: Improvements of Adhoc Overloading

[Makarius]

*** 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