fragment of a HOL type class primer --HG-- extra : rebase_source : c7ff6bceea8256c21b8b1f6081b53aad1df6c942