[isabelle] programming an instance proof in HOL

I wish to do the equivalent of

  instance tyop :: (class1) class2

I hoped that it would be enough to have (a certified term version of)

  Logic.mk_inclass (Type(tyop, [TFree("'a", [class1])]), class2)

as my goal.  Though I am able to prove this goal, I get an exception
when I attempt to add my new theorem as an arity (using

      ("add_arity: malformed type arity",
         ["OFCLASS('a bit0, asz2_class)"]) raised

What then should be the form of my theorem?

(I also tried using AxClass.add_classrel, but this fails with a
similar message.)


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