Re: [isabelle] instance theorems
My guess is that they're in the system
somewhere, as they need the same kind of theorem proving as
an ordinary lemma.
Currently, they are not stored. Moreover, some instance relations
between type constructors and sorts are not proven but inferred, proofs
would have to be constructed manually.
It is not out of scope to enrich axclass.ML in an appropriate manner,
but in order to understand your issue exactly, we would need more
context - can you send a description what you want to do exactly with
classes or a piece of code?
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
email;internet:florian.haftmann at informatik.tu-muenchen.de
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
This archive was generated by a fusion of
Pipermail (Mailman edition) and