[isabelle] Polymorphism and simple type



Hi,

I have a question about Isabelle's polymorphism. Since Isabelle has a
simply-typed lambda calculus, how come the meta-logic is polymorphic?
Polymorphism is not typically considered simple, right?

Regards
Steve




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.