[isabelle-dev] Theorem

[Marmsoler, Diego]

Dear Mailing List,

I just started developing in Isabelle/ML and I tried to consult the implementation manual but could not find an answer to my question so I will try to post it here.

I have a theorem which was proven in a certain local theory context (a locale in this case).
Now I want to use this theorem in another local theory context (an extension of the original locale).
However, when I try to use it for a proof in the new locale I get the following error message:

Undeclared hyps: xxx

(Here the xxx refers to some assumptions of the original locale)


Since the new locale is an extension of the original locale, I guess it should be possible to use the theorem in this new context but I could not figure out how.
Thus I was wondering if someone here has an idea of how I can import the theorem from the original locale to the extended one?

Thanks a lot for your help,

Diego

Diego Marmsoler
Lecturer (Education and Research), Computer Science
University of Exeter, Innovation 1, Room 10
www: marmsoler.com<http://www.marmsoler.com>
Twitter: @DiegoMarmsoler<https://twitter.com/DiegoMarmsoler>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240803/fcc4a596/attachment.htm>