[isabelle] Finding locale where some fact is originally defined
I have used sledgehammer to show:
lemma "x\<squnion>\<bottom> = x" by (metis bot_def bot_least
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" ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and