[isabelle] Finding locale where some fact is originally defined



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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.