[isabelle-dev] instantiation

Amine Chaieb ac638 at cam.ac.uk
Mon Oct 27 16:50:35 CET 2008


Dear all,

(How) Can I perform an instantiation of a type-constructor with two 
arguments, an thereby restricting them to be the same?

Concrete problem:

instantiation "fun" (type, type) power
begin
....

end


but I want only to raise functions of type 'a => 'a to powers.

Thank you for any hint!

best wishes,
Amine.


More information about the isabelle-dev mailing list