Re: [isabelle] power class instantiation



Unfortunately "set" is not a type constructor but an abbreviation for
"'a => bool". Hence you cannot instatiate any class with "set". For an
alternative search for ^^ in Nat.thy or Transitive_Closure.thy.

Tobias

Viorel Preoteasa schrieb:
> 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.