*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Finding locale where some fact is originally defined*From*: Christian Doczkal <c.doczkal at stud.uni-saarland.de>*Date*: Tue, 03 Feb 2009 17:26:10 +0100*In-reply-to*: <49872E63.1090602@uni-muenster.de>*References*: <49872E63.1090602@uni-muenster.de>

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**

**References**:**[isabelle] Finding locale where some fact is originally defined***From:*Peter Lammich

- Previous by Date: [isabelle] CALCULEMUS 2009 - Final Call for Reviewed Papers
- Next by Date: [isabelle] TPHOLs'09 Last Call for Papers
- Previous by Thread: [isabelle] Finding locale where some fact is originally defined
- Next by Thread: [isabelle] TPHOLs'09 Last Call for Papers
- Cl-isabelle-users February 2009 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list