[isabelle-dev] adhoc overloading
makarius at sketis.net
Thu Aug 1 17:04:39 CEST 2013
On Wed, 17 Jul 2013, Christian Sternagel wrote:
> in case anybody finds localized ad-hoc overloading useful.
Quite often it is just a matter to tell users about the existence of such
Do you feel like making an example theory, e.g.
src/HOL/ex/Adhoc_Overloading_Examples.thy or a short entry for the
isar-ref manual? E.g. somewhere here
Strictly speaking it is probably not HOL specific, but re-use of the Pure
type language within the object-logic is somehow part of the specific
More information about the isabelle-dev