[isabelle-dev] Quotient example with partiality?

[Makarius]

On Tue, 29 Nov 2011, Cezary Kaliszyk wrote:

> When developing the quotient package we included the infrastructure for 
> defining quotient types with partial equivalence relations, however 
> since one of the main uses was supposed to be nominal (where its always 
> reflexive) we did not test the partial functionality too much.

> I will try to draft an example partial quotient and get back to you.

Maybe this really old example of partial equivalence relations and 
typedefs is of some interest, at least as amusement:

http://isabelle.in.tum.de/repos/isabelle/file/Isabelle99/src/HOL/Quot/


 	Makarius