[isabelle] type class instantiation

I have problems to instantiate the recpower class for parametric types. E.g., I have defined substitutions as association lists from variables to terms

types ('f,'v)sub = "('v * ('f,'v)term)list"

Now I want to instantiate `sub' for the recpower class where the unit element is the empty substitution and multiplication is substitution composition. But already for

instantiation sub :: recpower begin

I get `Illegal type abbreviation: "Term.sub"'. What does that mean? Can I only instantiate types defined by `datatype'? How do I write the instantiation for parametric types (if possible at all)?


christian sternagel

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