[isabelle] instance theorems



Hello,

  This is a second request for a way to access the theorems produced
by the "instance" keyword.  My guess is that they're in the system
somewhere, as they need the same kind of theorem proving as
an ordinary lemma. I can figure out the terms, eg. <= on sets is subset,
but my ad-hoc reasoning with the axioms in the absence of proof
terms is not scaling well.  Is there any chance for a real  proof term?

Thank you,

Sean





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