Re: [isabelle] proof term request
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