Stream: Beginner Questions

Topic: ML command to list/print lemmas proven in current theory

view this post on Zulip Andrea Vezzosi (Sep 25 2023 at 10:40):

Hi, is there a way to print the lemmas proven so far in the current theory? I'm thinking of adding it to the end of a theory I check with isabelle server to have confirmation of the successfully proven lemmas as a message.

I'd also be open to alter the lemma proofs to include a command that prints a message when successful, is that possible/easier?

view this post on Zulip Xiaokun Luan (Oct 17 2023 at 05:54):

Hi Andrea, I found Global_Theory.all_thms_of might be helpful to you, check this. Maybe you need to filter the return value of this function by checking its prefix.

Last updated: Dec 21 2024 at 16:20 UTC