[isabelle] Ways to add a checking layer for Theories?

Hi all,

Just out of curiosity, and because I guess this may be worth in some circumstances, I wonder if there exist some recommended ways to add custom obligations to Theory design and make them checked. I mean kind of style check and design rules check.

As an example, one may want to require all Theories to not contain any partial functions. Is there a way to do this without externally re-parsing and re-interpreting *.thy files? (which would be too error‑prone by the way). Do the Isabelle system have provision to invoke such a layer, feeding it with a structure corresponding to the Theory interpretation?

Hope my question is clear enough (I'm not sure). If not, just ask me to reword it.

With thanks

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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