Re: [isabelle] Finding locale where some fact is originally defined



Hi

> 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" ?

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

-- 
Gruß
Christian Doczkal

Attachment: smime.p7s
Description: S/MIME cryptographic signature



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