[isabelle] types in higher order logic



Hi,

is type inhabitation decidable in Isabelle's higher order logic? I.e. given
any term t and type T, whether

G |- t : T

holds? Is Isabelle/HOL's type system basically Hindley-Milner?

- Gergely



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