[isabelle] Add class "term" to a type with ML



Hello,

I’m trying to create a command for defining types from FOL, inspired from typedef.ML in HOL, but my axioms do not unify with the theorems because the new type have no sorts and “term” is needed.

Can anybody help me with this?

Thank you,

Daniel de la Concepción



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