[isabelle] proof term request
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and