[isabelle] HOL.default typeclass?

Hi all,

HOL defines a typeclass default. What is the purpose of that? The only
instantiations are for unit (in Product_Type), and some instantiations
for nat splattered around various sessions.

What I need is a typeclass that gives me an *executable* default value,
is the default-typeclass the right one for that?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.