*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Locale parameters*From*: Clemens Ballarin <ballarin at in.tum.de>*Date*: Mon, 26 Sep 2011 22:20:16 +0200*In-reply-to*: <CAP0k5J6BfJ02BH-tBZ17cEq__A-xvJDF+L_ohHNLkJaGoYnSpA@mail.gmail.com>*References*: <CAP0k5J6BfJ02BH-tBZ17cEq__A-xvJDF+L_ohHNLkJaGoYnSpA@mail.gmail.com>*User-agent*: Internet Messaging Program (IMP) H3 (4.3.8)

Hi John,

[...] and I want to prove a lemma stating that the constant 'c' in L1 does not have the same value as the constant 'c' in L2: lemma lem1: "ALL a b. L1 c --> c = a & L2 c --> c = b & a ~= b"

!!c. ALL a b. (L1 c --> ((c = a & L2 c) --> (c = b & a ~= b))) What you want is a lemma like this: L1 a & L2 b --> a ~= b Clemens

**References**:**[isabelle] Locale parameters***From:*John Munroe

- Previous by Date: Re: [isabelle] Locale parameters
- Next by Date: [isabelle] Isabelle release candidate
- Previous by Thread: Re: [isabelle] Locale parameters
- Next by Thread: [isabelle] Instantiate schematic variable in apply-script
- Cl-isabelle-users September 2011 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