Re: [isabelle] Variables in locale assumptions



> 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






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.