*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Variables in locale assumptions*From*: Peter Lammich <lammich at in.tum.de>*Date*: Sat, 22 Feb 2014 10:47:57 +0100*In-reply-to*: <5307D560.3010508@inf.ethz.ch>*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>

> It's this type constraint that surprised me. The post by Makarius > explains it, but as a user I would prefer to have complete separation. > Is there a compelling reason why it's implemented as it is? > I frequently run into another instance of this problem, when writing something like: lemma foo: "x & y --> x" "x = y --> f x = f y" Note that foo(2) is: "?x::bool = ?y ...", which is usually not what was intended. -- Peter

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

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

- 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