*To*: Andreas Lochbihler <lochbihl at ipd.info.uni-karlsruhe.de>*Subject*: Re: [isabelle] Lemmas in locales*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Wed, 14 May 2008 12:26:34 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <482983BC.9010804@ipd.info.uni-karlsruhe.de>*References*: <482983BC.9010804@ipd.info.uni-karlsruhe.de>

On 13 May 2008, at 14:04, Andreas Lochbihler wrote:

locale loc begin definition a :: bool where "a == True" definition b :: bool where "b == a" lemma b_lemma: "b = True" unfolding b_def a_def .. lemmas a_lemma' = b_lemma[unfolded b_def] lemmas a_lemma = a_lemma' endInside the locale, "thm a_lemma'" gives "a = True" as expected,outside the locale, I get "b = True" for "thm loc.a_lemma'".Naturally, I would want loc.a_lemma' to be "a = True" outside thelocale, too.

Declarations as

lemmas a_lemma' = b_lemma[unfolded b_def]

Clemens

**References**:**[isabelle] Lemmas in locales***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Mixfix syntax with fewer arguments
- Next by Date: [isabelle] Research Position in Computer Science at The Australian National University
- Previous by Thread: [isabelle] Lemmas in locales
- Next by Thread: [isabelle] about th proof of protocol
- Cl-isabelle-users May 2008 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