*To*: Gerwin Klein <Gerwin.Klein at nicta.com.au>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Makarius <makarius at sketis.net>*Date*: Mon, 24 Feb 2014 23:23:54 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <alpine.LNX.2.00.1402242255440.26330@lxbroy10.informatik.tu-muenchen.de>*References*: <FC4BBC48012AB34DAF828891BA6076320A6BED6F@MBX21.d.ethz.ch>, <D85BDDB5-D8F4-4F4C-A578-35FD64B33584@cantab.net> <FC4BBC48012AB34DAF828891BA6076320A6BEE7C@MBX21.d.ethz.ch> <9B97784B-AE5E-4291-B2C0-4285E7894C11@gmail.com> <5307D560.3010508@inf.ethz.ch> <alpine.LNX.2.00.1402241348450.5131@lxbroy10.informatik.tu-muenchen.de> <6363A4A9-BAD9-44F4-8860-15A89157E23E@nicta.com.au> <alpine.LNX.2.00.1402242255440.26330@lxbroy10.informatik.tu-muenchen.de>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Mon, 24 Feb 2014, Makarius wrote:

On Mon, 24 Feb 2014, Gerwin Klein wrote:or if you need to constrain types?The 'constrains' element is easier to get rid of. I would like to seesome constructive proofs where you "need to constrain types", as yousay. This is usually just a workaround to specify locale type arguments,but if that would be supported directly, the need would go away.

- In locale expressions, instantiation replaces renaming. Parameters must be declared in a for clause. To aid compatibility with previous parameter inheritance, in locale declarations, parameters that are not 'touched' (instantiation position "_" or omitted) are implicitly added with their syntax at the beginning of the for clause.

Makarius

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

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

**Re: [isabelle] Variables in locale assumptions***From:*Jasmin Blanchette

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

**Re: [isabelle] Variables in locale assumptions***From:*Makarius

**Re: [isabelle] Variables in locale assumptions***From:*Makarius

- 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