Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Axioms used in a proof

Email Gateway (Aug 18 2022 at 16:46):

From: John Munroe <munddr@gmail.com>
Hi all,

Is there a way to retrieve all axioms used in the proof of some lemma
in ML? I'm trying to find a way to find a 'closure' of the axioms
used, so if the selected lemma uses another lemma as a fact, I'd like
to look up the axioms used in the proof in that other lemma as well.

Thanks
John

Last updated: Nov 21 2024 at 12:39 UTC