Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Finding locale where some fact is originally d...

view this post on Zulip Email Gateway (Aug 18 2022 at 13:00):

From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,

I have used sledgehammer to show:

context complete_lattice
begin
lemma "x\<squnion>\<bottom> = x" by (metis bot_def bot_least
sup_absorb1)

And then I wondered in which locales the used lemmas are defined.

Is there any way (apart from doing a grep over the .thy - files), to
find out in which locale some lemma is originally defined?
i.e. is there any command, that tells me that sup_absorb1 comes from
"upper_semilattice" and bot_least from "complete_lattice" ?

regards,
Peter

view this post on Zulip Email Gateway (Aug 18 2022 at 13:05):

From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hi

If you use ProofGeneral/Emacs use C-c C-f ("Find Theorems") and search
with eg. "name:bot_def" and the likes.
smime.p7s

Last updated: May 03 2024 at 04:19 UTC