src/HOL/Quotient.thy
changeset 45476 6f9e24376ffd
parent 44921 58eef4843641
child 45680 a61510361b89