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


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.