--- a/src/Doc/Isar_Ref/Spec.thy Sun Jan 26 22:45:57 2025 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Mon Jan 27 12:13:37 2025 +0100
@@ -1093,6 +1093,41 @@
lemma "Length ((a, b, c, d, e), ()) = 1" by simp
+section \<open>Overloaded constant abbreviations: adhoc overloading\<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.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>Incorporating ML code \label{sec:ML}\<close>
text \<open>