*To*: Van Staden Stephan <stephan.vanstaden at inf.ethz.ch>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Makarius <makarius at sketis.net>*Date*: Fri, 21 Feb 2014 18:33:17 +0100 (CET)*Cc*: John Wickerson <johnwickerson at cantab.net>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net> <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 21 Feb 2014, Van Staden Stephan wrote:

It's a free variable in each assumption. I would expect the assumptionsto be:(!!S R. pred S R) /\ (!!S R. pred R S) but what happens is apparently: (!!S R. pred S R /\ pred R S)The question is whether the free variables in an assumption are local tothe assumption or not. The locale tutorial suggests that they should belocal, but maybe I'm wrong.

Scratch.thy?) Makarius

**Follow-Ups**:**Re: [isabelle] Variables in locale assumptions***From:*bnord

**Re: [isabelle] Variables in locale assumptions***From:*Stephan van Staden

**References**:**[isabelle] Variables in locale assumptions***From:*Van Staden Stephan

**Re: [isabelle] Variables in locale assumptions***From:*John Wickerson

**Re: [isabelle] Variables in locale assumptions***From:*Van Staden Stephan

- Previous by Date: Re: [isabelle] Variables in locale assumptions
- Next by Date: Re: [isabelle] Variables in locale assumptions
- Previous by Thread: Re: [isabelle] Variables in locale assumptions
- Next by Thread: Re: [isabelle] Variables in locale assumptions
- Cl-isabelle-users February 2014 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