src/HOL/Library/Quotient_Type.thy
changeset 63750 9c8a366778e1
parent 61585 a9599d3d7610
child 69593 3dda49e08b9d