Re: [isabelle] proof term request



Hi Clemens,

  I mean the latter.  the proof tree is labeled, eg.

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

If this is the same in 2005, my request is still open.  I'll try to get
the new version working today.

Best,

Sean


On Jan 16, 2006, at 8:33 AM, Clemens Ballarin wrote:

Hi Sean,

apparently, you are using Isabelle 2004, which is not going to be modified any more.

Apart from that, I haven't understood whether you are talking about accessing the exported version of a locale theorem, which is added to the theorem database of the theory, or about the theorem that is added to the proof context when entering a locale via "theorem (in L)", say.

Clemens
--
Dr. Clemens Ballarin
Institut fuer Informatik, TU Muenchen
Boltzmannstr. 3, 85748 Garching, Germany
Phone: +49-89-289-17326, Fax: +49-89-289-17307
http://www4.in.tum.de/~ballarin/







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