Dear Isabelle users,
I have successfully proved a list of facts using a combination of List.foldl
and 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 ctxt
in the thm list
given to Proof.unfolding
.
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 thm
and Proof.context
?
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,
using ML
and 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?
Thanks,
Ciaran
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