Re: [isabelle] instance theorems



Dear Sean,

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?

Rgds.
Florian

--

PGP available:
http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de.pgp
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=
	
x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard



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