[isabelle-dev] instantiation

Tjark Weber webertj at in.tum.de
Wed Oct 29 06:46:44 CET 2008

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


More information about the isabelle-dev mailing list