[isabelle] Looking up Constants (ML-level)



Hi,

On the ML level, given a set of Isabelle Constants and a context/ theory, I'd like to look up

- If the constant is a datatype-constructor
- or, if it is a function
- if it is a function, I'd also like to look up its defining equations. Is there a more programatic way of doing this than relying on @thms{'f.simps'}?

Could someone please point me to the relevant bit of Isabelle where I can find some functions that does this?

Thanks,
Moa





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