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