[isabelle-dev] Quotient and typedef

2011-12-08 Thread Florian Haftmann
Dear all, since my post on quotient and partiality created some confusion, I want to cast some light on it from a more direct perspective. Concerning »typedef«, we currently have two conflicting issues: a) From a foundational perspective, we want to leave »typedef« untouched »as it is« b)

Re: [isabelle-dev] Quotient and typedef

2011-12-08 Thread Lukas Bulwahn
On 12/08/2011 02:35 PM, Florian Haftmann wrote: Dear all, since my post on quotient and partiality created some confusion, I want to cast some light on it from a more direct perspective. Just a few short comments from my side: Concerning »typedef«, we currently have two conflicting issues: