Dear Isabelle users,
I have successfully proved a list of facts using a combination of
Proof.theorem to yield a new context
ctxt with these theorems available.
I then want to prove some more facts, using the facts now available in
thm list given to
What is the best way for me to access the proved theorems?
I'm currently using
Global_Theory.get_thm and coercing the
lthy : local_theory into a
theory to retrieve them by name, which feels sloppy.
Is there a version of
Proof.theorem which returns a
When I try to proof my new facts using those available in
ctxt, the proof fails.
I have been able to successfully emulate what I'm trying to do in toplevel Isar,
local_setup keywords. But trying to do this within one ML function
has proved difficult.
I assume that I am handling my contexts in a poor fashion. Any advice?
Got it! I was building my new goal using the wrong term :rolling_eyes:, so my other facts didn't work.
Ciarán Dunne has marked this topic as resolved.
Last updated: Dec 07 2023 at 16:21 UTC