[isabelle] power class instantiation



Hello

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

instantiation "set" :: (power) power
begin

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.