*To*: Makarius <makarius at sketis.net>, Gerwin Klein <Gerwin.Klein at nicta.com.au>*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 25 Feb 2014 08:14:23 +0100*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*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

On 24/02/14 23:05, Makarius wrote:

The 'constrains' element is easier to get rid of. I would like to see some constructive proofs where you "need to constrain types", as you say. This is usually just a workaround to specify locale type arguments, but if that would be supported directly, the need would go away.

Andreas

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

**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: [isabelle] *Deadline extended* Final call for contributions AI4FM 2014
- 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