diff -r 846293abd12d -r 96afb0707532 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sun Jan 26 22:45:57 2025 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jan 27 12:13:37 2025 +0100
@@ -5,7 +5,6 @@
     Main
     "HOL-Library.Old_Datatype"
     "HOL-Library.Old_Recdef"
-    "HOL-Library.Adhoc_Overloading"
     "HOL-Library.Dlist"
     "HOL-Library.FSet"
     Base
@@ -648,41 +647,6 @@
 \<close>
 
 
-section \<open>Adhoc overloading of constants\<close>
-
-text \<open>
-  \begin{tabular}{rcll}
-  @{command_def "adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
-  @{command_def "no_adhoc_overloading"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
-  @{attribute_def "show_variants"} & : & \<open>attribute\<close> & default \<open>false\<close> \\
-  \end{tabular}
-
-  \<^medskip>
-  Adhoc overloading allows to overload a constant depending on its type.
-  Typically this involves the introduction of an uninterpreted constant (used
-  for input and output) and the addition of some variants (used internally).
-  For examples see \<^file>\<open>~~/src/HOL/Examples/Adhoc_Overloading_Examples.thy\<close> and
-  \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
-
-  \<^rail>\<open>
-    (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
-      (@{syntax name} (@{syntax term} + ) + @'and')
-  \<close>
-
-  \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
-  existing constant.
-
-  \<^descr> @{command "no_adhoc_overloading"} is similar to @{command
-  "adhoc_overloading"}, but removes the specified variants from the present
-  context.
-
-  \<^descr> @{attribute "show_variants"} controls printing of variants of overloaded
-  constants. If enabled, the internally used variants are printed instead of
-  their respective overloaded constants. This is occasionally useful to check
-  whether the system agrees with a user's expectations about derived variants.
-\<close>
-
-
 section \<open>Definition by specification \label{sec:hol-specification}\<close>
 
 text \<open>