Re: [isabelle] proof term request

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.

Dr. Clemens Ballarin
Institut fuer Informatik, TU Muenchen
Boltzmannstr. 3, 85748 Garching, Germany
Phone: +49-89-289-17326, Fax: +49-89-289-17307

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