[isabelle] proof term request



Hello,

I have a request to modify the proof terms from locales slightly. Right now, theorems which are proved in a locale setting, eg. Record.thy, only label the Thm parts of the proof tree with the short name of the theorem, eg. "induct", when this is suppose
to signify "Record.product_type.induct".
See, eg. the proof of "Record.product_type.surjective_pairing"
It is rather difficult to figure out when I'm
dealing with a locale theorem, and then I can imagine when two locales are open at once and this will be doubly confusing. Even if only one locale is open, it's an ugly
hack to figure out which "induct" you mean, as there are many.
Would marking the Thm nodes in this way be a problem? If so, please suggest
a workaround.

Thanks,

Sean





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