[isabelle] power class instantiation


I need to instantiate the class power to sets, something like:

instantiation "set" :: (power) power

definition "one = {1}"
definition "A * B = {x . ? a in A . ? b in B . x = a * b}
However I get an error in the first line of this declaration.

*** Logical type constructor expected: "set"
*** At command "instantiation".

Best regards,

Viorel Preoteasa

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