Re: [isabelle] proof term request



Sean McLaughlin wrote:

PThm(("Record.product_type.induct",_),...)

OK. But note that things are not a simple as that. In general, theorems added to the context are instances of theorems stored in the locale. Additionally, if the theorem was generated via interpretation (commands interpretation and interpret) its hypotheses are replaced by hypotheses of the context.

Clemens





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