Overloading is a core feature of Isabelle's logic. It allows you to declare a single constant with a "broad" type that can be defined on specific types. There's rarely a need for users to do that manually. It is the underlying mechanism used to implement type classes. For example, if you define a type class as follows:
class empty =
fixes empty :: 'a
assumes (* ... *)
Then, the class command will declare the constant empty of type 'a', and subsequent instantiations merely provide a definition of empty for specific types, like nat or list.
Long story short: overloading is – for most purposes – an implementation detail that is managed by higher-level commands. Occasionally, the need for some manual tweaking arises, e.g. when you have to define a type that depends on class constraints.
Ad-hoc overloading is, in my opinion, a misleading name. As far as I understand, it stems from Haskell (see this paper from Wadler and Blott). There, they use it to describe precisely the type class mechanism that in Isabelle would be coined as just "overloading". In Isabelle, ad-hoc overloading means something entirely different. The idea is that you can use it to define abstract syntax (like do-notation for monads) that can't accurately be capture by Isabelle's ML-style simple type system. As in overloading, you'd define a constant with a "broad" type. But that constant never receives any definitions! Instead, you define new constants with more specific types. When Isabelle's term parser encounters the use of the abstract constant, it will try to replace it with a concrete constant.
For example: you can use do-notation with option, list, and a few other types. If you write something like:
do { x <- foo; bar }
Then Isabelle sees:
Monad_Syntax.bind foo (%x. bar)
In a second step, depending on the type of foo, it will translate it to one of these possible terms:
Option.bind foo (%x. bar)
List.bind foo (%x. bar)
(* ... more possibilities ...*)
Again, users probably don't need to deal with this concept explicitly. If you pull in Monad_Syntax from the library, you'll get one application of ad-hoc overloading readily configured.
Long story short: ad-hoc overloading is a mechanism for enabling "fancy" syntax in Isabelle. Newbies may get confused by it because error messages tend to be hard to understand if there's something wrong in the internal translation.
