On Mon, 2008-10-27 at 16:53 +0100, Florian Haftmann wrote: > Amine Chaieb schrieb: > > (How) Can I perform an instantiation of a type-constructor with two > > arguments, an thereby restricting them to be the same? > > This is beyond the type class system of Isabelle. A pity.
While this may not give you what you wanted, you can of course state
(and trivially prove)
lemma "OFCLASS('a => 'a, power_class)"
by intro_classes
Best,
Tjark
