src/HOL/Quotient.thy
changeset 45509 624872fc47bf
parent 44921 58eef4843641
child 45680 a61510361b89