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
"x & y --> x"
"x = y --> f x = f y"
Note that foo(2) is: "?x::bool = ?y ...", which is usually not
what was intended.
This archive was generated by a fusion of
Pipermail (Mailman edition) and